Abbreviations do not work - Githubissues

leanprover-community / lean4web

The Lean 4 web editor

https://live.lean-lang.org/

Apache License 2.0

52 stars 14 forks source link

Abbreviations do not work #9

Closed joneugster closed 7 months ago

joneugster commented 7 months ago

Some lean-abbreviations seem not to work

\in
anything not starting in a letter, like \<<

joneugster commented 7 months ago

Fixed in c21db2d