Documentation

Init.Data.Array.FinRange

source
def Array.finRange (n : Nat) :
Array (Fin n)

Returns an array of all elements of Fin n in order, starting at 0.

Examples:

Equations
    Instances For
      source
      @[simp]
      theorem Array.size_finRange {n : Nat} :
      (Array.finRange n).size = n
      source
      @[simp]
      theorem Array.getElem_finRange {n i : Nat} (h : i < (Array.finRange n).size) :
      (Array.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
      source
      @[simp]
      theorem Array.finRange_zero :
      Array.finRange 0 = #[]
      source
      theorem Array.finRange_succ {n : Nat} :
      Array.finRange (n + 1) = #[0] ++ map Fin.succ (Array.finRange n)
      source
      theorem Array.finRange_succ_last {n : Nat} :
      Array.finRange (n + 1) = map Fin.castSucc (Array.finRange n) ++ #[Fin.last n]
      source
      theorem Array.finRange_reverse {n : Nat} :
      (Array.finRange n).reverse = map Fin.rev (Array.finRange n)