Def Vector.removeNth

Modification history

2024-05-06 07:35

Mathlib/Data/Vector.lean

chore: migrate from `List.removeNth` to `List.eraseIdx` (#12660)

Deleted Vector.removeNth View on Github →

2022-12-12 18:44

Mathlib/Data/Vector.lean

feat: port Data.Vector from lean-core (#834) …

Added Vector.removeNth View on Github →