# Function declarations¶

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

In the following example, we define a function `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.Data.Nat;
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 arguments is used.

The following function has two clauses.

```
open import Stdlib.Data.Bool;
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 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`

.

```
open import Stdlib.Data.Nat;
open import Stdlib.Data.Bool;
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;
```

## 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 `λ`

.

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

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

## Short definitions¶

A function definition can be written in one line, with the body immediately following the signature:

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