11.3. Finite Natural Numbers

Planned Content

Tracked at issue #169

structure

Fin (n : Nat) : Type

Fin n is a natural number i with the constraint that 0 ≤ i < n. It is the "canonical type with n elements".

Constructor

Fin.mk

Creates a Fin n from i : Nat and a proof that i < n.

`val`	`:`	`Nat`
		If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be written as `i.1` or just `i` when the target type is known.
`isLt`	`:`	`↑self < n`
		If `i : Fin n`, then `i.2` is a proof that `i.1 < n`.