Zulip Chat Archive
Stream: mathlib4
Topic: Data.Array.Lemmas PR !4#2194
Shreyas Srinivas (Feb 10 2023 at 16:34):
Topic for this port PR. Before pushing to this branch please check here.
Notification Bot (Feb 13 2023 at 15:31):
6 messages were moved from this topic to #mathlib4 > has_to_tactic_format by Eric Wieser.
Shreyas Srinivas (Feb 22 2023 at 15:15):
What is the lean4 version of heq_of_heq_of_eq from lean3
Eric Wieser (Feb 22 2023 at 16:45):
Shreyas Srinivas (Feb 22 2023 at 17:00):
that is the lean3 version
Eric Wieser (Feb 22 2023 at 17:07):
Ok, docs4#heq_of_heq_of_eq is the Lean4 version. I'm confused how you couldn't find it when it has the same name
Shreyas Srinivas (Feb 22 2023 at 17:45):
I went around looking for HEq_... etc. (since that is the mathlib4 name for heq)
Shreyas Srinivas (Feb 22 2023 at 17:46):
mathlib3port's version also had a different name
Reid Barton (Feb 22 2023 at 17:50):
Lean 4 names are like German verbs, you have to know how they decline in all the different positions.
Reid Barton (Feb 22 2023 at 17:52):
So it is HEq as a type, but heq when it appears in the name of a theorem
Reid Barton (Feb 22 2023 at 17:53):
And they are irregular, so you cannot predict either one from the other.
Shreyas Srinivas (Feb 22 2023 at 17:55):
But this does not appear to apply to names of data structures like lists. toList _.. theorems for example
Kevin Buzzard (Feb 22 2023 at 18:54):
Yeah, that's the power of the naming convention. I have long given up trying to understand it. I figure it will just make sense to me one day. I just trust that the people who made the convention know what they're talking about.
Last updated: Dec 20 2023 at 11:08 UTC