Skip to content

Commit 3b43156

Browse files
authored
doc: correct grammar error in array indexing panic message (#11368)
This PR corrects a grammar error in a docstring in the GetElem file for array indexing.
1 parent 644a217 commit 3b43156

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/GetElem.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
116116

117117
/--
118118
The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
119-
panics `i` is out of bounds.
119+
panics if `i` is out of bounds.
120120
-/
121121
macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
122122

0 commit comments

Comments
 (0)