-- This module introduces operators. module Introduction.Operators where -- Agda has a very flexible mechanism for defining operators, supporting infix, -- prefix, postfix and mixfix operators. data Nat : Set where zero : Nat suc : Nat -> Nat -- Any name containing underscores (_) can be used as an operator by writing -- the arguments where the underscores are. For instance, the function _+_ is -- the infix addition function. This function can be used either as a normal -- function: '_+_ zero zero', or as an operator: 'zero + zero'. _+_ : Nat -> Nat -> Nat zero + m = m suc n + m = suc (n + m) -- A fixity declaration specifies precedence level (50 in this case) and -- associativity (left associative here) of an operator. Only infix operators -- (whose names start and end with _) have associativity. infixl 50 _+_ -- The only restriction on where _ can appear in a name is that there cannot be -- two underscores in sequence. For instance, we can define an if-then-else -- operator: data Bool : Set where false : Bool true : Bool if_then_else_ : {A : Set} -> Bool -> A -> A -> A if true then x else y = x if false then x else y = y -- if_then_else_ is treated as a prefix operator (ends, but doesn't begin with -- an _), so the declared precedence determines how something in an else branch -- should be parsed. For instance, with the given precedences -- if x then y else a + b -- is parsed as -- if x then y else (a + b) -- and not -- (if x then y else a) + b infix 10 if_then_else_ -- In Agda there is no restriction on what characters are allowed to appear in -- an operator (as opposed to a function symbol). For instance, it is allowed -- (but not recommended) to define 'f' to be an infix operator and '+' to be a -- function symbol. module BadIdea where _f_ : Nat -> Nat -> Nat zero f zero = zero zero f suc n = suc n suc n f zero = suc n suc n f suc m = suc (n f m) + : Nat -> Nat + n = suc n