Lemmas about List.range
and List.enum
#
Ranges and enumeration #
range' #
@[reducible, inline, deprecated List.range'_eq_singleton_iff (since := "2025-01-29")]
Instances For
range #
iota #
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
zipIdx #
enumFrom #
@[deprecated List.zipIdx_eq_append_iff (since := "2025-01-21")]