Skip to content

Commit

Permalink
doc: fix typo and omission (#3614)
Browse files Browse the repository at this point in the history
* Capitalize the first letter of the docstring of `String.leftpad`.
* Enclose in backticks 'A' in the docstring of `String.head`.
  • Loading branch information
chabulhwi committed Apr 26, 2023
1 parent 39ecb3b commit 8dafb51
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Data/String/Defs.lean
Expand Up @@ -19,7 +19,7 @@ This file defines a bunch of functions for the `String` datatype.

namespace String

/-- pad `s : String` with repeated occurrences of `c : Char` until it's of length `n`.
/-- Pad `s : String` with repeated occurrences of `c : Char` until it's of length `n`.
If `s` is initially larger than `n`, just return `s`. -/
def leftpad (n : Nat) (c : Char) (s : String) : String :=
⟨List.leftpad n c s.data⟩
Expand Down Expand Up @@ -82,7 +82,7 @@ def popn (s : String) (n : Nat) : String :=
⟨s.toList.drop n⟩
#align string.popn String.popn

/-- Produce the head character from the string `s`, if `s` is not empty, otherwise 'A'. -/
/-- Produce the head character from the string `s`, if `s` is not empty, otherwise `'A'`. -/
def head (s : String) : Char :=
s.iter.curr
#align string.head String.head
Expand Down

0 comments on commit 8dafb51

Please sign in to comment.