Mixfix

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