Stream: Coq devs & plugin devs

Topic: Constant/MutInd API


view this post on Zulip Hugo Herbelin (Dec 20 2021 at 19:03):

Am I the only ones having troubles to remember what Constant.make, Constant.make1, Constant.make2 are doing? What about the following alternatives:

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.

view this post on Zulip Gaëtan Gilbert (Dec 20 2021 at 19:48):

I like n°3 best

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2021 at 22:24):

Would it make sense to have somethin glike Constant.Canonical.t ?

view this post on Zulip Gaëtan Gilbert (Dec 20 2021 at 22:33):

what would that be?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 21 2021 at 00:18):

A projection?

view this post on Zulip Hugo Herbelin (Dec 21 2021 at 09:20):

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: Feb 06 2023 at 20:02 UTC