In stdlib, we have at least 6 different ways of naming things related to Type
when something analogous exists for Prop
:
sig
-> sigT
Logic
-> Logic_Type
excluded_middle
-> excluded_middle_informative
not_Zeq
-> not_Zeq_inf
relation
-> crelation
nat_ind
-> nat_rect
It could be nice to have it more uniform. Any opinion or historical justification for one or another choice?
inf is bad because it looks like infinity
crelation is bad because who knows what the c is even supposed to mean
I think T
-ending is nice, it's short and unmistakenable
I quite like sig
-> sigT
although I am guilty of defining things called ...T
that have nothing to do with Prop
versus Type
.
I was adopting fooT
/ foo.t
as an OCaml-inspired suffix for data types, tho those are usually Set
s or Type
s.
If you want more than 1 letter, Ty
seems rather unambiguous.
Also, even if T
might be used elsewhere, adding T
to a Prop
probably remains unambiguous.
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.
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: Sep 30 2023 at 15:01 UTC