**See the official user manual for the most up-to-date version of the information on this page.**

<< this needs to be completed>>

If a name of a function contains one or more underscores (_) it can be used as an operator with the arguments going where the underscores are. Consequently, the function _+_ can be used as an infix operator writing n + m for _+_ n m. There are (almost) no restrictions on what symbols are allowed as operator names, for instance we can define

_and_ : Bool -> Bool -> Bool true and x = x false and _ = false if_then_else_ : {A : Set} -> Bool -> A -> A -> A if true then x else y = x if false then x else y = y

Such a function can be called using the arguments in their mixfix places, or using prefix notation, so

(if_then_else_) c x y

is equivalent to

if x then x else y

Page last modified on December 14, 2018, at 06:46 PM

Powered by
PmWiki