Documentation

Std.Data.Fin.Basic

theorem Fin.pos {n : Nat} (i : Fin n) :
0 < n
@[inline]
def Fin.last (n : Nat) :
Fin (n + 1)

The greatest value of Fin (n+1).

Instances For
@[inline]
def Fin.castLT {m : Nat} {n : Nat} (i : Fin m) (h : i.val < n) :
Fin n

castLT i h embeds i into a Fin where h proves it belongs into.

Instances For
@[inline]
def Fin.castLE {n : Nat} {m : Nat} (h : n m) (i : Fin n) :
Fin m

castLE h i embeds i into a larger Fin type.

Instances For
@[inline]
def Fin.cast {n : Nat} {m : Nat} (eq : n = m) (i : Fin n) :
Fin m

cast eq i embeds i into an equal Fin type.

Instances For
@[inline]
def Fin.castAdd {n : Nat} (m : Nat) :
Fin nFin (n + m)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

Instances For
@[inline]
def Fin.castSucc {n : Nat} :
Fin nFin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

Instances For
def Fin.addNat {n : Nat} (i : Fin n) (m : Nat) :
Fin (n + m)

addNat m i adds m to i, generalizes Fin.succ.

Instances For
def Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) :
Fin (n + m)

natAdd n i adds n to i "on the left".

Instances For
@[inline]
def Fin.rev {n : Nat} (i : Fin n) :
Fin n

Maps 0 to n-1, 1 to n-2, ..., n-1 to 0.

Instances For
@[inline]
def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m i.val) :
Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

Instances For
@[inline]
def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i 0) :
Fin n

Predecessor of a nonzero element of Fin (n+1).

Instances For
def Fin.clamp (n : Nat) (m : Nat) :
Fin (m + 1)

min n m as an element of Fin (m + 1)

Instances For