Agda[0] and Coq and other languages for formalising mathematics (they are also programming languages) make a lot of use of Unicode to make the mathematical stat

Agda[0] and Coq and other languages for formalising mathematics (they are also programming languages) make a lot of use of Unicode to make the mathematical statements readable. Here is an example: > ∑-+-distribute : ∑ (A + B) C ≃ (∑ A (C ∘ left)) + (∑ B (C ∘ right)) This is quite readable and would be understandable to someone who did not know Agda or the library in particular, but who understood the subject material. If the characters were replaced by words the overhead would be big. The Plan9 operating system invented the compose key, which makes writing unicode characters easy enough for anyone to use them. Unfortunately, it requires a bit of setup to make the compose key work in X on Linux or *BSD (I have described th process here[1]). Agda and Coq therefore use special input modes for Emacs and other editors. I also use Unicode in my Latex documents to make them more readable. [2] [0]: https://agda.readthedocs.io/en/latest/getting-started/quick-guide.html#writing-mathematical-symbols-in-source-code https://agda.readthedocs.io/en/latest/getting-started/quick-... [1]: https://hakon.gylterud.net/tutorials/unicode.html https://hakon.gylterud.net/tutorials/unicode.html [2]: https://hakon.gylterud.net/tutorials/latex-maths-unicode.html https://hakon.gylterud.net/tutorials/latex-maths-unicode.htm...