3 ms·
It goes further. Agda allows mixfix operators [0], which allows expressions to be arbitrarily interleaved with names and symbols, e.g.: if_then_else_ : {A
by bradrn 5y ago
It goes further. Agda allows mixfix operators [0], which allows expressions to be arbitrarily interleaved with names and symbols, e.g.:
if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y
[0] https://agda.readthedocs.io/en/v2.6.0.1/language/mixfix-operators.html https://agda.readthedocs.io/en/v2.6.0.1/language/mixfix-oper...
- agumonkey 5y agoHey that's lifted from Smalltalk isn't it ?
- dragonwriter 5y agoSmalltalk has functions with keyword arguments that look kind of like mixfix operators.
- travisgriggs 5y agoI miss keyword syntax. It has its warts, but I liked the clarity better than the whole funarg() list mess.
- agumonkey 5y agofunny, googling mixfix taught me racket also had something for it https://docs.racket-lang.org/mixfix/ https://docs.racket-lang.org/mixfix/