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

@[inline]

def Fin.foldl {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) : α

Folds over Fin n from the left: foldl 3 f x = f (f (f x 0) 1) 2.

Equations

• Fin.foldl n f init = Fin.foldl.loop n f init 0

def Fin.foldl.loop {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (x : α) (i : Nat) : α

Inner loop for Fin.foldl. Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)

Equations

• Fin.foldl.loop n f x i = if h : i < n then Fin.foldl.loop n f (f x { val := i, isLt := h }) (i + 1) else x

@[inline]

def Fin.foldr {α : Sort u_1} (n : Nat) (f : Fin n → α → α) (init : α) : α

Folds over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)).

Equations

• Fin.foldr n f init = Fin.foldr.loop n f { val := n, property := (_ : n ≤ n) } init

def Fin.foldr.loop {α : Sort u_1} (n : Nat) (f : Fin n → α → α) : { i : Nat // i ≤ n } → α → α

Inner loop for Fin.foldr. Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))

Equations

• Fin.foldr.loop n f { val := 0, property := property } x = x
• Fin.foldr.loop n f { val := Nat.succ i, property := h } x = Fin.foldr.loop n f { val := i, property := (_ : i ≤ n) } (f { val := i, isLt := h } x)