Lemmas about Vector.range'
, Vector.range
, and Vector.zipIdx
#
Ranges and enumeration #
range' #
@[simp]
theorem
Vector.range'_succ
(s n step : Nat)
:
range' s (n + 1) step = Vector.cast ⋯ ({ toArray := #[s], size_toArray := ⋯ } ++ range' (s + step) n step)
@[simp]