-
Notifications
You must be signed in to change notification settings - Fork 388
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
doc: add docstrings and examples for String
functions
#4332
Conversation
Mathlib CI status (docs):
|
Add docstrings, usage examples, and doctests for `String.get'`, `String.next'`, `String.posOf`, `String.revPosOf`.
d9585bb
to
29adfc1
Compare
src/Init/Data/String/Basic.lean
Outdated
Given `def abc := "abc"` and `def lean := "L∃∀N"`, | ||
* `abc.get' 0 (by decide) = 'a'` | ||
* `lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
May clearer without the defs, and just inlining the strings?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
and below.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I updated the single "abc"
case. I agree this is more apparent.
I have streamlined the repetitive examples by replacing the "Given, def...
" line with a let statement in the bullet:
`let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'`
It seems off to me to inline the string in the repetitive cases:
`"L∃∀N".get' (0 |> "L∃∀N".next |> "L∃∀N".next) (by decide) = '∀'`.
However, please let me know if you still prefer the inlining in the repetitive cases, and I will update the examples accordingly.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, thanks.
Otherwise, looks good. |
awaiting-review |
Add docstrings, usage examples, and doctests for
String.get'
,String.next'
,String.posOf
,String.revPosOf
.