Patrick Massot
Patrick Massot
Leo asked for help from the community to write docstrings in the Lean 4 codebase. It would be nice to have a docstring style guide to help in this effort...
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
Fixes #150 and helps mitigating the effects of #157 The goal is to allow data tables attached to steps as described in https://cucumber.io/docs/reference#data-tables. This has nothing to do with example...
Should we somehow run the mathlib linters on the core library. For instance it would catch `mul_nonneg` which uses forbidden inequalities.
When opening a game folder and editing a script file from there, nothing shows up in the outline. If I open a single script.rpy then I see the outline. This...
Copy-pasting from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/MIL.20comments to make sure we don't forget 2.2: In the example at the end if one "feels cocky": Normally I would prove mul_right_inv before proving mul_one. Maybe this...
From Zulip: > Another general remark about my tutorials: I never tell my students about simp. That would be too powerful, and it would encourage them to try simp every...
We need to explain the `finset` vs `fintype` vs `finite` mess somewhere, probably in Chapter 4.
Do we want to explain the `rintros ⟨⟩` trick somewhere?
Not an actual issue up to now, but let's record that we should carefully monitor https://github.com/leanprover-community/mathlib/pull/3083