Hi,
I'm trying to port a project to mathcomp 2/HB following the recommended porting guide.
According to the guide, canonical structures are represented in mathcomp 2 via hierarchy builder instances, i.e., they are created via HB.instance
.
But instances are never named. In fact, the guide states that they should not be named to let the hierarchy builder do the job of finding the canonical instance:
Note that the instance need not be named and better not be since it is the job of HB to figure out instances automatically.
But the guide never says how I can actually use a canonical instance of a structure for a certain type.
For example, assume I would like to define a cast from unit
to choiceType
:
Definition cast (t:unit) : choiceType := t.
Here, I would like to use the canonical instance for unit
. I thought maybe the coercions that HB generates would do this job for me but that does not seem to be the case.
What am I missing?
Hi @Sebastian Ertel supposing you could name the canonical choice type for unit (e.g. unit_choiceType : choiceType
, what would your cast
function look like now?
Anyway, with HB and Coq >= 8.16 (and preferably >= 8.18 because of printing features), you can now write unit : choiceType
to mean the choiceType
structure on unit
, formerly called unit_choiceType
or [choiceType of unit]
.
E.g. you may define Definition unit_choiceType : choiceType := unit
.
Hi @Cyril Cohen ,
thanks for your response.
Definition unit_choiceType : choice := unit.
gives me the following error:
The term "unit" has type "Type" while it is expected to have type "choiceType".
Also Definition unit_choiceType : choiceType := [choiceType of unit].
gives me the following error:
The term "id_phant" has type "phantom Type unit → phantom Type unit" while it is expected to have type "unify Type Type unit ?cT nomsg".
I'm on Coq 8.18 and mathcomp 2.1.0.
You probably need to From mathcomp Require Import choice.
?
No, I do have that already.
(Otherwise using choiceType
itself would already fail resolution.)
Then we would need a minimal example to understand because here, the following works:
From mathcomp Require Import ssreflect ssrfun ssrbool choice.
Check unit : choiceType.
Hi @Pierre Roux ,
Indeed what you wrote there is the minimal example. It fails for me with
The term "unit" has type "Type" while it is expected to have type "choiceType".
Let me prepare a nix flake that I can share.
Yes, that indeed sounds like some bad version of something.
Last updated: Oct 13 2024 at 01:02 UTC