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
Instances For
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 : α)
: