max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(emacs/lean-input): add shortcuts for alpha, beta and gamma

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-17 11:46:26 -08:00
parent dfd2a23cd4
commit b7a4f305d4
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-input.el
View file

@ -620,6 +620,10 @@ order for the change to take effect."
("H" . ("ℍ"))
("K" . ("𝕂"))
("a" . ("α"))
("b" . ("β"))
("g" . ("γ"))
;; Musical symbols.
("note" . ,(lean-input-to-string-list "♩♪♫♬"))