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

fix: find? -> findRev? (#11514)

Browse source 
This PR fixes a small oversight in a docstring.
This commit is contained in:
Paul Reichert 2025-12-05 08:36:32 +01:00 • committed by GitHub
parent 455fd0b448
commit f2415b7a9a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/List/Basic.lean
View file

@ -1607,8 +1607,8 @@ such element is found.
`O(|l|)`.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 2`
* `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
* `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
* `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
-/
def findRev? (p : α → Bool) : List α → Option α
| [] => none