Am I the only ones having troubles to remember what Constant.make
, Constant.make1
, Constant.make2
are doing? What about the following alternatives:
KerName.make
):Constant.make2
-> Constant.make
(with an optional ~user:modpath
)Constant.make1
-> Constant.of_kn
(with an optional ~user:modpath
, or optional ~user:kn
)Constant.make
-> subsumed by Constant.of_kn ~user:modpath
Scheme 2 ( to follow the model of KerName.make
, but less disruptive):
Constant.make2
-> Constant.make
Constant.make1
-> Constant.of_kn
Constant.make
-> Constant.of_kn2
(or Constant.of_kn_pair
)Scheme 3 (to suggest that make1
/make2
are building a canonical name):
Constant.make2
-> Constant.make_canonical
Constant.make1
-> Constant.make_canonical_of_kn
Constant.make
-> Constant.make_pair
(or unchanged)Scheme 4 (to oppose buiding a pair of different or same names):
Constant.make2
-> Constant.make_same
Constant.make1
-> Constant.make_same_of_kn
Constant.make
-> Constant.make_pair
(or unchanged)Additionally, when looking at when these functions are used, one can see that it is often to do low-level manipulation to implement higher-level functionalities such as is_canonical : Constant.t -> bool
, or canonize : Constant.t -> Constant.t
. So, I'm considering providing those too. Any opinion? In particular, by doing so, the need for another cryptic name, Constant.repr2
, disappears.
Same for MutInd
of course.
I like n°3 best
Would it make sense to have somethin glike Constant.Canonical.t
?
what would that be?
A projection?
For the record #15391 implements scheme 1 and this branch implements scheme 3. Also, a variant for scheme 1 would be to have not ~user
but ~canonical
optional.
Last updated: Jun 04 2023 at 19:30 UTC