# Function declarations¶

A function declaration consists of a type signature followed by a group
of *function clauses*.

In the following example, we define a function `multiplyByTwo`

.

```
import Stdlib.Data.Nat open using {Nat; *};
multiplyByTwo : Nat -> Nat
| n := 2 * n;
```

The first line `multiplyByTwo : Nat -> Nat`

is the type signature and the
second line `| n := 2 * n;`

is a function clause.

## Pattern matching¶

A function may have more than one function clause. When a function is called, it will pattern match on the input, and the first clause that matches the arguments is used.

The following function has two clauses:

```
import Stdlib.Data.Bool open;
neg : Bool -> Bool
| true := false
| 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`

.

## Short definitions¶

Initial function arguments that are matched against variables or wildcards in all clauses can be moved to the left of the colon in the function definition. For example,

```
import Stdlib.Data.Nat open;
add (n : Nat) : Nat -> Nat
| zero := n
| (suc m) := suc (add n m);
```

is equivalent to

```
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
| n zero := n
| n (suc m) := suc (add n m);
```

If there is only one clause with no patterns, then the pipe `|`

must be omitted:

```
import Stdlib.Data.Nat open;
multiplyByTwo (n : Nat) : Nat := n;
```

## Mutually recursive functions¶

Function declarations can depend on each other 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`

.

```
import Stdlib.Data.Nat open;
import Stdlib.Data.Bool open;
import Stdlib.Prelude open;
odd : Nat -> Bool
| zero := false
| (suc n) := even n;
even : Nat -> Bool
| zero := true
| (suc n) := odd n;
```

Identifiers do not need to be defined before they are used. Then it is possible to define mutually recursive functions/types without any special syntax.

However, there are some exceptions to this. We cannot forward reference a symbol
`f`

in some statement `s`

if between `s`

and the definition of `f`

there is one
of the following statements:

- Local module
- Import statement
- Open statement

## Anonymous functions¶

Anonymous functions, or *lambdas*, are introduced with the syntax:

```
\{| pat1 .. patN_1 := clause1
| ..
| pat1 .. patN_M := clauseM }
```

The first pipe `|`

is optional. Instead of `\`

one can also use the Unicode
alternative – `λ`

.

An anonymous function just lists all clauses of a function without naming it. Any function declaration can be converted to use anonymous functions:

```
import Stdlib.Prelude open;
odd : Nat -> Bool :=
\ {
| zero := false
| (suc n) := even n
};
even : Nat -> Bool :=
\ {
| zero := true
| (suc n) := odd n
};
```