@[implicit_reducible]

def List.finRange (n : Nat) : List (Fin n)

Lists all elements of Fin n in order, starting at 0.

Examples:

• List.finRange 0 = ([] : List (Fin 0))
• List.finRange 2 = ([0, 1] : List (Fin 2))

Equations

• List.finRange n = List.ofFn fun (i : Fin n) => i

@[simp]

theorem List.length_finRange {n : Nat} : (finRange n).length = n

@[simp]

theorem List.getElem_finRange {n i : Nat} (h : i < (finRange n).length) : (finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩

@[simp]

theorem List.finRange_zero : finRange 0 = []

theorem List.finRange_succ {n : Nat} : finRange (n + 1) = 0 :: map Fin.succ (finRange n)

theorem List.finRange_succ_last {n : Nat} : finRange (n + 1) = map Fin.castSucc (finRange n) ++ [Fin.last n]

theorem List.finRange_reverse {n : Nat} : (finRange n).reverse = map Fin.rev (finRange n)

@[simp]

theorem List.mem_finRange {n : Nat} (x : Fin n) : x ∈ finRange n

theorem Fin.foldlM_eq_foldlM_finRange {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin n → m α) (x : α) : foldlM n f x = List.foldlM f x (List.finRange n)

theorem Fin.foldrM_eq_foldrM_finRange {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) : foldrM n f x = List.foldrM f x (List.finRange n)

theorem Fin.foldl_eq_finRange_foldl {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : foldl n f x = List.foldl f x (List.finRange n)

theorem Fin.foldr_eq_finRange_foldr {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : foldr n f x = List.foldr f x (List.finRange n)

theorem List.ofFnM_succ {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : ofFnM f = do let a ← f 0 let as ← ofFnM fun (i : Fin n) => f i.succ pure (a :: as)