Relatively easy in Vim with digraphs (:h digraph) Ctrl-K l* produces λ Ctrl-K L* produces Λ Unsurprisingly, Emacs also supports this when programming in Agda

Relatively easy in Vim with digraphs (:h digraph) Ctrl-K l* produces λ Ctrl-K L* produces Λ Unsurprisingly, Emacs also supports this when programming in Agda (\lambda) i'm not sure if it's a builtin feature or part of the Agda plugin. In Agda using Unicode identifiers is widely accepted, even in the standard library: https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary.agda https://github.com/agda/agda-stdlib/blob/master/src/Relation...