[Merged by Bors] - chore: avoid lean3 style have/suffices#6964
[Merged by Bors] - chore: avoid lean3 style have/suffices#6964
Conversation
|
I personally think the style with |
|
I think both styles are fine. @semorrison what do you see as the downside of the style? |
|
I think this is a lean3-ism, which unnecessarily introduces an intermediate tactic state with multiple goals (immediately before the This PR originated because I made a PR upstreaming the tactic supporting this style to Std, and @digama0 (correctly, I think!) told me this was a bad idea. Supporting this syntax also makes parsing slightly more complicated, because Lean has to decide whether the core syntax or the overriden syntax from Mathlib is relevant. Of course it can cope, but why not make it unambiguous? I think everything is better about the new style, and we should consciously move on from lean3-isms where possible, rather than holding on to them out of familiarity. |
|
One reason not to do this manually is that this syntactic transformation is within the realm of things we could do automatically (once we get full library syntax rewrites working). |
|
Sorry, why is that a reason to not do it? Are you asking that this be left as a warm-up / practice problem for full library rewrites? |
|
It's fine if you want to do it now, but it might be a waste of work if a computer will soon automate the job. |
|
I wasn't proposing to do anymore than are already here. |
|
I have always difficulties with the syntax for |
sgouezel
left a comment
There was a problem hiding this comment.
It's clearly much better like that, thanks!
bors d+
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
bors merge |
Many proofs use the "stream of consciousness" style from Lean 3, rather than `have ... := ` or `suffices ... from/by`. This PR updates a fraction of these to the preferred Lean 4 style. I think a good goal would be to delete the "deferred" versions of `have`, `suffices`, and `let` at the bottom of `Mathlib.Tactic.Have` (Anyone who would like to contribute more cleanup is welcome to push directly to this branch.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Many proofs use the "stream of consciousness" style from Lean 3, rather than `have ... := ` or `suffices ... from/by`. This PR updates a fraction of these to the preferred Lean 4 style. I think a good goal would be to delete the "deferred" versions of `have`, `suffices`, and `let` at the bottom of `Mathlib.Tactic.Have` (Anyone who would like to contribute more cleanup is welcome to push directly to this branch.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Many proofs use the "stream of consciousness" style from Lean 3, rather than
have ... :=orsuffices ... from/by.This PR updates a fraction of these to the preferred Lean 4 style.
I think a good goal would be to delete the "deferred" versions of
have,suffices, andletat the bottom ofMathlib.Tactic.Have(Anyone who would like to contribute more cleanup is welcome to push directly to this branch.)