Languages like Agda allow → or -> interchangeably in the body of the code: https://agda.readthedocs.io/en/v2.5.2/language/lexical-structure.html#tokens https://

Languages like Agda allow → or -> interchangeably in the body of the code: https://agda.readthedocs.io/en/v2.5.2/language/lexical-structure.html#tokens https://agda.readthedocs.io/en/v2.5.2/language/lexical-struc... Most languages only allow such symbols in strings, though, so it's pretty simple: - Symbols outside of a string literal are ligatures. - Symbols inside strings are the real symbol. Ligatures are also rendered differently to any similar unicode characters.