Skip to content

Commit

Permalink
doc: fix typo
Browse files Browse the repository at this point in the history
Co-authored-by: David Thrane Christiansen <[email protected]>
  • Loading branch information
austinletson and david-christiansen committed May 7, 2024
1 parent 48c0723 commit 1f0f5eb
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/String/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ the result is unspecified.
Examples:
* `"abc".next ⟨1⟩ = String.Pos.mk 2`
* `"L∃∀N".next ⟨1⟩ = String.Pos.mk 4`
`'∃'` is a mutli-byte character
`'∃'` is a multi-byte character
Cases where the result is unspecified:
* `"abc".next ⟨3⟩`, since `3 = s.endPos`
Expand Down

0 comments on commit 1f0f5eb

Please sign in to comment.