Cannot input character "∎" (U+220E END OF PROOF)

banacorn / agda-mode

agda-mode on Atom

https://atom.io/packages/agda-mode

MIT License

58 stars 14 forks source link

Cannot input character "∎" (U+220E END OF PROOF) #45

Closed exists-forall closed 7 years ago

exists-forall commented 7 years ago

The character "∎" (U+220E END OF PROOF) is necessary to end equational reasoning blocks, but there is no ASCII input sequence to type this character using agda-mode. It appears that the emacs version of agda-mode uses \qed for this purpose. Would it be possible for this package to do the same?

banacorn commented 7 years ago

@danilkolikov has also addressed this in #44 earlier this week.

After some investigation, I found that, along with 5 other symbols (\geq, \leq, \bullet, \qed, \par and \newline), they were all excluded by the keymap generator for some reason I have yet to recall XD