Further lemmas about List.take
, List.drop
, List.zip
and List.zipWith
. #
These are in a separate file from most of the list lemmas
as they required importing more lemmas about natural numbers, and use omega
.
take #
@[reducible, inline, deprecated List.take_set_of_le (since := "2025-02-04")]
Equations
Instances For
drop #
Dropping the elements up to i
in l₁ ++ l₂
is the same as dropping the elements up to i
in l₁
, dropping the elements up to i - l₁.length
in l₂
, and appending them.
findIdx #
findIdx? #
takeWhile #
rotateLeft #
@[simp]
rotateRight #
@[simp]