clamp #
enum/list #
foldl #
theorem
Fin.foldl_loop_lt
{α : Sort u_1}
{n : Nat}
{m : Nat}
(f : α → Fin n → α)
(x : α)
(h : m < n)
:
Fin.foldl.loop n f x m = Fin.foldl.loop n f (f x ⟨m, h⟩) (m + 1)
theorem
Fin.foldl_loop_eq
{α : Sort u_1}
{n : Nat}
(f : α → Fin n → α)
(x : α)
:
Fin.foldl.loop n f x n = x
@[irreducible]
theorem
Fin.foldl_loop
{α : Sort u_1}
{n : Nat}
{m : Nat}
(f : α → Fin (n + 1) → α)
(x : α)
(h : m < n + 1)
:
Fin.foldl.loop (n + 1) f x m = Fin.foldl.loop n (fun (x : α) (i : Fin n) => f x i.succ) (f x ⟨m, h⟩) m
theorem
Fin.foldl_eq_foldl_list
{α : Type u_1}
{n : Nat}
(f : α → Fin n → α)
(x : α)
:
Fin.foldl n f x = List.foldl f x (Fin.list n)
foldr #
theorem
Fin.foldr_loop_zero
{n : Nat}
{α : Sort u_1}
(f : Fin n → α → α)
(x : α)
:
Fin.foldr.loop n f ⟨0, ⋯⟩ x = x
theorem
Fin.foldr_loop_succ
{n : Nat}
{α : Sort u_1}
{m : Nat}
(f : Fin n → α → α)
(x : α)
(h : m < n)
:
Fin.foldr.loop n f ⟨m + 1, h⟩ x = Fin.foldr.loop n f ⟨m, ⋯⟩ (f ⟨m, h⟩ x)
theorem
Fin.foldr_eq_foldr_list
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : α)
:
Fin.foldr n f x = List.foldr f x (Fin.list n)