You also can use mixfix syntax [1] if you want extensible syntax. [1] https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix https://wiki.portal.chalmers.

You also can use mixfix syntax [1] if you want extensible syntax. [1] https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix It is used by Agda and Maude and is quite versatile. Note that one of examples above is if_then_else_ function which implements a typical language construct, but in Agda, due to lasiness, it is just an ordinary function. [2] https://news.ycombinator.com/item?id=20697414 https://news.ycombinator.com/item?id=20697414 McCarthy did not understand lambda calculus at the time he specified Lisp and what can be a function became a special form, if I not mistaken. So, for another approach at extensible syntax you may consider mixfix notation and lazy evaluation.