max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update some Array doc-strings (#6832)

Browse source
This commit is contained in:
Kim Morrison 2025-01-29 12:32:41 +11:00 • committed by GitHub
parent 9b5fadd275
commit 07e2b7d913
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Data/Array/Basic.lean
View file

@ -856,12 +856,19 @@ it has to backshift all elements at positions greater than `i`. -/
def eraseIdx! (a : Array α) (i : Nat) : Array α :=
if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
/-- Remove a specified element from an array, or do nothing if it is not present.
This function takes worst case O(n) time because
it has to backshift all later elements. -/
def erase [BEq α] (as : Array α) (a : α) : Array α :=
match as.indexOf? a with
| none => as
| some i => as.eraseIdx i
/-- Erase the first element that satisfies the predicate `p`. -/
/-- Erase the first element that satisfies the predicate `p`.
This function takes worst case O(n) time because
it has to backshift all later elements. -/
def eraseP (as : Array α) (p : α → Bool) : Array α :=
match as.findIdx? p with
| none => as