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

chore: correct doc-string for Array.swap! (#4869)

Browse source
This commit is contained in:
Kim Morrison 2024-07-31 14:02:30 +10:00 • committed by GitHub
parent 688da9d8a7
commit 8acdafd5b3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -108,7 +108,7 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
a'.set (size_set a i v₂ ▸ j) v₁
/--
Swaps two entries in an array, or panics if either index is out of bounds.
Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
This will perform the update destructively provided that `a` has a reference
count of 1 when called.