-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/fin): add docs; fin_zero_elim -> fin.elim0; fin_zero_elim' -> fin_zero_elim #2055
Conversation
Also drom `fin_zero_elim` in favor of `fin.elim0` from `stdlib` and rename `fin_zero_elim'` to `fin_zero_elim`.
src/data/fin.lean
Outdated
| 0 i := i.elim0 | ||
| (succ n) ⟨0, _⟩ := H0 _ | ||
| (succ n) ⟨succ i, h⟩ := Hs _ _ (succ_rec ⟨i, lt_of_succ_lt_succ h⟩) | ||
|
||
/-- Define `C n i` by induction on `i : fin n` interpreted as `(0 : fin (n - i)).succ.succ…`, |
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.
This is a little confusing. For one, Hs
isn't introduced in the doc string. It's not immediately clear what the ...
is doing. Instead of the short one-line description, could you maybe expand it to a few sentences that make it clearer how to use the definition?
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.
Reformulated. Is it better?
Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>
…> fin_zero_elim (leanprover-community#2055) * doc(data/fin): add some docs Also drom `fin_zero_elim` in favor of `fin.elim0` from `stdlib` and rename `fin_zero_elim'` to `fin_zero_elim`. * Update src/data/fin.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update docs, fix `Π` vs `∀`. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…> fin_zero_elim (leanprover-community#2055) * doc(data/fin): add some docs Also drom `fin_zero_elim` in favor of `fin.elim0` from `stdlib` and rename `fin_zero_elim'` to `fin_zero_elim`. * Update src/data/fin.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * Update docs, fix `Π` vs `∀`. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Also drom
fin_zero_elim
in favor offin.elim0
fromstdlib
andrename
fin_zero_elim'
tofin_zero_elim
.Are there any theorems in
data/fin
worth mentioning in the module docstring?TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list