9.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 {n : Nat} (val : Nat) (isLt : val < n)
    : Fin n

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

`isLt`	:	`↑self < n`
		If `i : Fin n`, then `i.2` is a proof that `i.1 < 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.