|
|
|
|
|
|
by danidiaz
2563 days ago
|
|
|
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... |
|
|