Basic properties of List.eraseIdx
#
List.eraseIdx l k
erases k
-th element of l : List α
.
If k ≥ length l
, then it returns l
.
Alias of the reverse direction of List.eraseIdx_eq_self
.
List.eraseIdx
#List.eraseIdx l k
erases k
-th element of l : List α
.
If k ≥ length l
, then it returns l
.
Alias of the reverse direction of List.eraseIdx_eq_self
.