Stream: Coq devs & plugin devs

Topic: [stdlib] Naming convention for moving from Prop to Type


view this post on Zulip Olivier Laurent (Dec 03 2021 at 13:05):

In stdlib, we have at least 6 different ways of naming things related to Type when something analogous exists for Prop:

It could be nice to have it more uniform. Any opinion or historical justification for one or another choice?

view this post on Zulip Gaëtan Gilbert (Dec 03 2021 at 13:18):

inf is bad because it looks like infinity
crelation is bad because who knows what the c is even supposed to mean

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2021 at 13:20):

I think T-ending is nice, it's short and unmistakenable

view this post on Zulip Janno (Dec 03 2021 at 13:20):

I quite like sig -> sigT although I am guilty of defining things called ...T that have nothing to do with Prop versus Type.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 14:19):

I was adopting fooT / foo.t as an OCaml-inspired suffix for data types, tho those are usually Sets or Types.

view this post on Zulip Alexander Gryzlov (Dec 03 2021 at 14:25):

If you want more than 1 letter, Tyseems rather unambiguous.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 14:29):

Also, even if T might be used elsewhere, adding T to a Prop probably remains unambiguous.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 14:31):

And we could probably update most of the cases above easily with deprecations — except for sigT and nat_rect, changes there would break almost everything.

view this post on Zulip Matthieu Sozeau (Dec 10 2021 at 19:32):

Gaëtan Gilbert said:

inf is bad because it looks like infinity
crelation is bad because who knows what the c is even supposed to mean

It's supposed to mean computational


Last updated: Feb 01 2023 at 15:04 UTC