Zulip Chat Archive

Stream: general

Topic: Lean4 lemma names


view this post on Zulip Patrick Massot (Feb 17 2020 at 10:09):

@Sebastian Ullrich Unless I misunderstood, in Pittsburgh you told us there was not yet a naming convention for lemma names in Lean 4. But https://github.com/leanprover/lean4/commit/db3d9c9284dfb9b27dfa17214d7c3c2ce7409f08 suggests this is no longer true. Do you have any comment here? My understanding was that we could hope to keep lean 3 underscore separated names.

view this post on Zulip Sebastian Ullrich (Feb 17 2020 at 10:15):

@Patrick Massot It's not something we have explicitly decided on yet, at least. We should probably start that discussion by now.

view this post on Zulip Patrick Massot (Feb 17 2020 at 10:59):

Great! Can I respectfully suggest another discussion topic that seems timely? As a user and teacher using Lean, it would be nice if intro and cases were the powerfull mathlib versions or if it were possible for mathlib to completely replace the core lib intro and cases without having a different name (and without hacks).

view this post on Zulip Mario Carneiro (Feb 17 2020 at 11:21):

One problem is that cases has an incompatible syntax with rcases, so if we replace it then we will need to keep cases_old around or change the formatting everywhere

view this post on Zulip Johan Commelin (Feb 17 2020 at 11:30):

Or we make the parser just a bit more complex to figure out which of the two syntaxes is used. Because I think they can be distinguished.

view this post on Zulip Patrick Massot (Feb 17 2020 at 12:28):

My hope is it's not too late to change everywhere. I expect there are currently very few proofs using the interactive cases tactic in Lean 4.

view this post on Zulip Patrick Massot (Feb 17 2020 at 12:29):

(if any)

view this post on Zulip Sebastian Ullrich (Feb 17 2020 at 12:44):

Patrick Massot said:

or if it were possible for mathlib to completely replace the core lib intro and cases without having a different name (and without hacks).

That version sounds reasonable. It's the same customization story we want to have for other parts of the language (commands, terms, ...) as well.

view this post on Zulip Patrick Massot (Feb 17 2020 at 12:45):

Indeed, that would be consistent with everything else.

view this post on Zulip Patrick Massot (Feb 17 2020 at 12:45):

And that would be the most flexible solution, as planned with the whole Lean 4 story.


Last updated: May 17 2021 at 21:12 UTC