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) :
    (finRange n)[i] = Fin.cast i, h