Zulip Chat Archive

Stream: mathlib4

Topic: Some naming questions

Patrick Massot (Oct 16 2022 at 19:26):

I'm working on data.prod.basic and I have a couple of naming questions. mathport and I were both surprised by capitalization in Function.injective, Function.surjective, and Function.bijective. It seems those names were added by @Kevin Buzzard in https://github.com/leanprover-community/mathlib4/pull/13/files. Should we change the capitalization? Should we rather add an alignment directive somewhere?

Patrick Massot (Oct 16 2022 at 19:28):

mathport is also confused by capitalization in decidable_of_decidable_of_iff, but this is a lemma from core.

Kevin Buzzard (Oct 16 2022 at 19:55):

Probably they were added when there was still a discussion about the naming convention for lean 4

Patrick Massot (Oct 16 2022 at 19:57):

This is likely, but I'll wait for Mario or Gabriel's approval before renaming all this.

Mario Carneiro (Oct 16 2022 at 20:15):

Yes, definitions that are props are pascal-cased

Mario Carneiro (Oct 16 2022 at 20:15):

so Function.Injective

Patrick Massot (Oct 16 2022 at 20:16):

Do you should I should simply restart translating that file?

Patrick Massot (Oct 16 2022 at 20:16):

I mean starting from the mathport output

Mario Carneiro (Oct 16 2022 at 20:17):

That's up to you

Mario Carneiro (Oct 16 2022 at 20:18):

I generally prefer the human changes over the machine version, but if the human version wasn't based on mathport at all then many things could be missing

Patrick Massot (Oct 16 2022 at 20:19):

I suspect it wasn't based on mathport at all. @Kevin Buzzard could you confirm?

Mario Carneiro (Oct 16 2022 at 20:20):

in that case it's probably easier to start over

Kevin Buzzard (Oct 16 2022 at 20:23):

I think I was just practicing lean 4

Kevin Buzzard (Oct 16 2022 at 20:24):

This is so low down in the heirarchy that some stuff is in lean 3 and some in mathlib, I was just trying to get things working if I recall correctly

Scott Morrison (Oct 16 2022 at 22:00):

I'd suggest that for any file that isn't already a "complete port", we take "starting over" as the default route.

This might involve:

  • move the existing X.lean to X2.lean
  • take X.lean from mathlib3port, and get it working as X.lean
  • import X.lean in X2.lean
  • delete everything in X2.lean that by now has already been defined in X.lean
  • find homes for or discard anything that remains (judgement required here!)
  • get everything downstream working again

mathport would ideally do some of this work for us, but doesn't yet.

Last updated: Dec 20 2023 at 11:08 UTC