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).

Equations

• Fin.last n = { val := n, isLt := (_ : n < Nat.succ n) }

@[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.

Equations

• Fin.castLT i h = { val := i.val, isLt := h }

@[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.

Equations

• Fin.castLE h i = { val := i.val, isLt := (_ : i.val < m) }

@[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.

Equations

• Fin.cast eq i = { val := i.val, isLt := (_ : i.val < m) }

@[inline]

def Fin.castAdd {n : Nat} (m : Nat) : Fin n → Fin (n + m)

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

Equations

• Fin.castAdd m = Fin.castLE (_ : n ≤ n + m)

@[inline]

def Fin.castSucc {n : Nat} : Fin n → Fin (n + 1)

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

Equations

• Fin.castSucc = Fin.castAdd 1

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

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

Equations

• Fin.addNat i m = { val := i.val + m, isLt := (_ : i.val + m < n + m) }

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

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

Equations

• Fin.natAdd n i = { val := n + i.val, isLt := (_ : n + i.val < n + m) }

@[inline]

def Fin.rev {n : Nat} (i : Fin n) : Fin n

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

Equations

• Fin.rev i = { val := n - (i.val + 1), isLt := (_ : n - (i.val + 1) < n) }

@[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.

Equations

• Fin.subNat m i h = { val := i.val - m, isLt := (_ : i.val - m < n) }

@[inline]

def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n

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

Equations

• Fin.pred i h = Fin.subNat 1 i (_ : 0 < i.val)

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

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

Equations

• Fin.clamp n m = { val := min n m, isLt := (_ : min n m < Nat.succ m) }