Agda does, but it also supports a plain ascii hyphen in identifiers. It allows operator characters inside identifiers and requires spaces around operators other

Agda does, but it also supports a plain ascii hyphen in identifiers. It allows operator characters inside identifiers and requires spaces around operators otherwise (as proposed in the article). So you can use x-y as an identifier: x-y : ℤ → ℤ → ℤ x-y x y = x - y The Agda community also heavily uses unicode characters. I've even seen a unicode colon used for a custom syntax because the ascii colon was unavailable.