search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

Issues with some symbolic shortcuts #30

Closed rkirsling closed 9 years ago

rkirsling commented 9 years ago

Some of the backslash shortcuts aren't producing their expected output in the online editor.

According to the table in Chapter 3.3 of the tutorial:

In the first case, \lr works as expected (as does \<-> and \leftrightarrow), but \iff produces ⇔ instead, which results in an unexpected token error. The cause here seems to be input-method.js#L689.

The second case is weirder: \neg works correctly (as does \lnot), but \not produces U+0338, a sort of "combining slash" character. Looking at input-method.js#L701 though, nothing really seems amiss. :confused:

soonhokong commented 9 years ago

@rkirsling, I moved this to https://github.com/leanprover/tutorial/issues/81