# Safe Array Indices

The `GetElem`

instance for `Array`

and `Nat`

requires a proof that the provided `Nat`

is smaller than the array.
In practice, these proofs often end up being passed to functions along with the indices.
Rather than passing an index and a proof separately, a type called `Fin`

can be used to bundle up the index and the proof into a single value.
This can make code easier to read.
Additionally, many of the built-in operations on arrays take their index arguments as `Fin`

rather than as `Nat`

, so using these built-in operations requires understanding how to use `Fin`

.

The type `Fin n`

represents numbers that are strictly less than `n`

.
In other words, `Fin 3`

describes `0`

, `1`

, and `2`

, while `Fin 0`

has no values at all.
The definition of `Fin`

resembles `Subtype`

, as a `Fin n`

is a structure that contains a `Nat`

and a proof that it is less than `n`

:

```
structure Fin (n : Nat) where
val : Nat
isLt : LT.lt val n
```

Lean includes instances of `ToString`

and `OfNat`

that allow `Fin`

values to be conveniently used as numbers.
In other words, the output of `#eval (5 : Fin 8)`

is `5`

, rather than something like `{val := 5, isLt := _}`

.

Instead of failing when the provided number is larger than the bound, the `OfNat`

instance for `Fin`

returns a value modulo the bound.
This means that `#eval (45 : Fin 10)`

results in `5`

rather than a compile-time error.

In a return type, a `Fin`

returned as a found index makes its connection to the data structure in which it was found more clear.
The `Array.find`

in the previous section returns an index that the caller cannot immediately use to perform lookups into the array, because the information about its validity has been lost.
A more specific type results in a value that can be used without making the program significantly more complicated:

```
def findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Fin arr.size × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (⟨i, h⟩, x)
else findHelper arr p (i + 1)
else none
termination_by findHelper arr p i => arr.size - i
def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) :=
findHelper arr p 0
```

## Exercise

Write a function `Fin.next? : Fin n → Option (Fin n)`

that returns the next largest `Fin`

when it would be in bounds, or `none`

if not.
Check that

```
#eval (3 : Fin 8).next?
```

outputs

```
some 4
```

and that

```
#eval (7 : Fin 8).next?
```

outputs

```
none
```