In Agda, if_then_else_ is a ternary operator: https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix https://wiki.portal.chalmers.se/agda/ReferenceManual/M

In Agda, if_then_else_ is a ternary operator: https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix https://wiki.portal.chalmers.se/agda/ReferenceManual/Mixfix For Agda being lazily evaluated, ternary if_then_else_ corresponds to usual if cond then true_expr else else_expr syntax of most mainstream languages. Maude also have a lot of infix, prefix, postfix and mixfix, including ternary operations: https://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/maude-manual_31.html https://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/ma...