take and drop #
Further results on List.take
and List.drop
, which rely on stronger automation in Nat
,
are given in Init.Data.List.TakeDrop
.
@[reducible, inline, deprecated List.take_set (since := "2025-02-17")]
Further results on List.take
and List.drop
, which rely on stronger automation in Nat
,
are given in Init.Data.List.TakeDrop
.