Skip to content

Commit

Permalink
doc: remove link from docstring
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Feb 20, 2024
1 parent fe94546 commit eb17dbc
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions src/Init/Prelude.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2375,10 +2375,7 @@ Indexing a `String` by a byte position is constant-time, while codepoint
positions need to be translated internally to byte positions in linear-time.
A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p`
lies on a UTF8 byte boundary. This notion is properly introduced in [std's
`String.Pos.Valid`][valid].
[valid]: https://leanprover-community.github.io/mathlib4_docs/Std/Data/String/Lemmas.html#String.Pos.Valid
lies on a UTF8 byte boundary.
-/
structure String.Pos where
/-- Get the underlying byte index of a `String.Pos` -/
Expand Down

0 comments on commit eb17dbc

Please sign in to comment.