On 6/1/2023 6:49 AM, Timon Gehr wrote: > I am just using the Agda input mode in emacs, so e.g., I just type "\to" and I > get "→", "\'a" and I get "á", etc. https://agda.readthedocs.io/en/v2.6.3/tools/emacs-mode.html https://github.com/DigitalMars/med/blob/master/src/med/more.d#L350