From ecae85e77bfc5dce0efaa7cc4fa6798d14f0c3be Mon Sep 17 00:00:00 2001 From: Benjamin Shi Date: Mon, 10 Nov 2025 18:04:07 +0800 Subject: [PATCH] doc: fix typo in `List.finIdxOf?` (#11111) This PR fixes a typo in the doc string of `List.finIdxOf?`. The first line of the doc string previously says the function returns the size of the list if no element equal to `a`, but both the examples in the doc string and real run-time behavior indicate it returns `none` in this case. Closes #11110 --- src/Init/Data/Array/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 3f8144e3c8..9ea3b17fc0 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -1295,7 +1295,7 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega /-- -Returns the index of the first element equal to `a`, or the size of the array if no element is equal +Returns the index of the first element equal to `a`, or `none` if no element is equal to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds. Examples: