Skip to content

Commit dfa5306

Browse files
committed
fix: use {lit} role for underscore in documentation
1 parent 776680e commit dfa5306

File tree

2 files changed

+5
-5
lines changed

2 files changed

+5
-5
lines changed

src/Init/Data/String/Slice.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1249,7 +1249,7 @@ def foldr {α : Type u} (f : Char → α → α) (init : α) (s : Slice) : α :=
12491249
Checks whether the slice can be interpreted as the decimal representation of a natural number.
12501250
12511251
A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
1252-
it are digits. Underscores (`_`) are allowed as digit separators for readability, but cannot appear
1252+
it are digits. Underscores ({lit}`_`) are allowed as digit separators for readability, but cannot appear
12531253
at the start, at the end, or consecutively.
12541254
12551255
Use {name (scope := "Init.Data.String.Slice")}`toNat?` or
@@ -1293,7 +1293,7 @@ Interprets a slice as the decimal representation of a natural number, returning
12931293
{name}`none` if the slice does not contain a decimal natural number.
12941294
12951295
A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
1296-
it are digits. Underscores (`_`) are allowed as digit separators and are ignored during parsing.
1296+
it are digits. Underscores ({lit}`_`) are allowed as digit separators and are ignored during parsing.
12971297
12981298
Use {name}`isNat` to check whether {name}`toNat?` would return {name}`some`.
12991299
{name (scope := "Init.Data.String.Slice")}`toNat!` is an alternative that panics instead of
@@ -1322,7 +1322,7 @@ Interprets a slice as the decimal representation of a natural number, returning
13221322
slice does not contain a decimal natural number.
13231323
13241324
A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
1325-
it are digits. Underscores (`_`) are allowed as digit separators and are ignored during parsing.
1325+
it are digits. Underscores ({lit}`_`) are allowed as digit separators and are ignored during parsing.
13261326
13271327
Use {name}`isNat` to check whether {name}`toNat!` would return a value. {name}`toNat?` is a safer
13281328
alternative that returns {name}`none` instead of panicking when the string is not a natural number.

src/Init/Data/String/Substring.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -403,7 +403,7 @@ Examples:
403403
Checks whether the substring can be interpreted as the decimal representation of a natural number.
404404
405405
A substring can be interpreted as a decimal natural number if it is not empty and all the characters
406-
in it are digits. Underscores (`_`) are allowed as digit separators for readability, but cannot appear
406+
in it are digits. Underscores ({lit}`_`) are allowed as digit separators for readability, but cannot appear
407407
at the start, at the end, or consecutively.
408408
409409
Use `Substring.toNat?` to convert such a substring to a natural number.
@@ -429,7 +429,7 @@ Checks whether the substring can be interpreted as the decimal representation of
429429
returning the number if it can.
430430
431431
A substring can be interpreted as a decimal natural number if it is not empty and all the characters
432-
in it are digits. Underscores (`_`) are allowed as digit separators and are ignored during parsing.
432+
in it are digits. Underscores ({lit}`_`) are allowed as digit separators and are ignored during parsing.
433433
434434
Use `Substring.isNat` to check whether the substring is such a substring.
435435
-/

0 commit comments

Comments
 (0)