Documentation

Init.Data.List.FinRange

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

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

Examples:

Equations
    Instances For
      @[simp]
      @[simp]
      theorem List.getElem_finRange {n i : Nat} (h : i < (finRange n).length) :
      theorem Fin.foldlM_eq_foldlM_finRange {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : αFin nm α) (x : α) :
      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 : α) :
      theorem Fin.foldl_eq_finRange_foldl {α : Type u_1} {n : Nat} (f : αFin nα) (x : α) :
      theorem Fin.foldr_eq_finRange_foldr {n : Nat} {α : Type u_1} (f : Fin nαα) (x : α) :
      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 af 0 let asofFnM fun (i : Fin n) => f i.succ pure (a :: as)