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

finRange n lists all elements of Fin n in order

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 : Nat} (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)