Zulip Chat Archive

Stream: general

Topic: Naming of equivs


Bryan Gin-ge Chen (Dec 08 2020 at 17:48):

In #5263, @Eric Wieser suggests the following rename:

-def dart_equiv_sigma : G.dart ≃ Σ v, G.neighbor_set v :=
+def dart.to_sigma : G.dart ≃ Σ v, G.neighbor_set v :=

I think this is in keeping with some recent changes where we've been "upgrading" various functions to *_equivs while naming them after the function rather than including equiv. However, I think it'd be good to get some more opinions here (and maybe we could draft something about this for our naming conventions doc?).

Bryan Gin-ge Chen (Dec 08 2020 at 18:26):

The main point against this I suppose is that it might not then be immediately clear from the name that the declaration actually has extra structure and that we're using a coercion.

Bhavik Mehta (Dec 08 2020 at 18:35):

I think it could also be confusing to have two possible names for one thing: in some cases the equiv is called an equiv and other times it's named to_ as in the function, so whichever is decided on should be made consistent through mathlib if possible

Eric Wieser (Dec 08 2020 at 19:12):

In the context of a tactic state, the coercion is usually obvious thanks to \u= arrows everywhere

Yury G. Kudryashov (Dec 08 2020 at 20:43):

Naming it dart.to_sigma allows us to write x.to_sigma.

Kyle Miller (Dec 09 2020 at 00:32):

This particular equivalence only exists to establish a fintype that @[derive fintype] wasn't able to automatically handle. I don't think it's very useful outside of that, since (bending the API a little...) d.is_adj is definitionally a proof that d.snd is an element of G.neighbor_set d.fst.

I was thinking that this should have equiv in the name because the existence of the equivalence itself is what's important, where the examples in mathlib that use to_ seem to be functions with a built-in inverse. (Or I could inline it into the fintype instance to simplify the naming problem :smile:)


Last updated: Dec 20 2023 at 11:08 UTC