Function declaration

A function declaration is a type signature and a group of definitions called function clauses.

In the following example we define a function called multiplyByTwo. The first line multiplyByTwo : Nat -> Nat; is the type signature and the second line multiplyByTwo n := 2 * n; is a function clause.

open import Stdlib.Prelude;

multiplyByTwo : Nat -> Nat;
multiplyByTwo n := 2 * n;

A function may have more than one function clause. When a function is called, the first clause that matches the argument is used.

The following function has two clauses.

open import Stdlib.Prelude;

neg : Bool -> Bool;
neg true := false;
neg false := true;

When neg is called with true the first clause is used and the function returns false. Similarly, when neg is called with false the second clause is used and the function returns true.

Mutually recursive functions

Function declarations can depend on others recursively. In the following example we define a function that checks if a number is even by calling a function that checks if a number is odd.

open import Stdlib.Prelude;

odd : Nat → Bool;

even : Nat → Bool;

odd zero := false;
odd (suc n) := even n;

even zero := true;
even (suc n) := odd n;