search

sagemathinc / cocalc

CoCalc: Collaborative Calculation in the Cloud
https://CoCalc.com
Other
1.17k stars 216 forks source link

Full range of Unicode symbols for Lean in CoCalc #4634

Closed vaibhavkarve closed 1 month ago

vaibhavkarve commented 4 years ago

Lean notation frequently uses the same keystrokes to bind several variants in the editor. For example, typing in \r in Emacs (in lean-mode) pulls up a menu where I can choose between any of the following: → ⇒ ⇛ ⇉ ⇄ ↦ ⇨ ↠ ⇀ ⇁ ⇢ ⇻ ↝ ⇾

All these symbols are defined here: https://github.com/leanprover/lean-mode#unicode

Currently, the CoCalc editor defaults to using only the first symbol from the list corresponding to each keystroke. Can we add support for the entire selection?

williamstein commented 1 month ago

People can use LEAN in cocalc via vscode with a compute server on cocalc. We'll very likely deprecate our custom lean editor and support soon.

https://github.com/sagemathinc/cocalc-howto/blob/main/lean.md