fin

Fin

data Fin : Nat -> Type

A natural number below n.

Fin.absurdZero

def absurdZero {A : Type} (i : Fin zero) : A

There is no index below zero.

Fin.toNat

def toNat {n : Nat} (i : Fin n) : Nat

The number.

Fin.ofNat

def ofNat (n : Nat) (k : Nat) (below : Nat.blt k n = true) : Fin n

The index of a number below the bound.

Fin.ofNatOption

def ofNatOption (n : Nat) (k : Nat) : Option (Fin n)

The index of a number, if it is below the bound.

Fin.last

def last (n : Nat) : Fin (succ n)

The largest index below succ n, which is n.

Fin.weaken

def weaken {n : Nat} (i : Fin n) : Fin (succ n)

The same number under a bound one larger.

Fin.beq

def beq {n : Nat} (i : Fin n) (j : Fin n) : Bool

Whether two indices are the same number.

Fin.blt

def blt {n : Nat} (i : Fin n) (j : Fin n) : Bool

Whether i is below j.

Fin.all

def all (n : Nat) : List (Fin n)

All the indices below n, in order.

Fin.toNatBelow

def toNatBelow {n : Nat} (i : Fin n) : Nat.blt (toNat i) n = true

An index’s number is below its bound.

Fin.toNatOfNat

def toNatOfNat (n : Nat) (k : Nat) (below : Nat.blt k n = true) : toNat (ofNat n k below) = k

An index made from a number has that number.

Fin.toNatWeaken

def toNatWeaken {n : Nat} (i : Fin n) : toNat (weaken i) = toNat i

Weakening keeps the number.

Fin.toNatLast

def toNatLast (n : Nat) : toNat (last n) = n

The last index below succ n is n.

Fin.allLength

def allLength (n : Nat) : List.length (all n) = n

There are n indices below n.