Julien Puydt (Oct 17 2022 at 12:29): Julien Puydt (Oct 17 2022 at 12:29):I'm sure the following doesn't work, and I'm not sure it's even going in the direction I want:
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp.
HB.mixin Record MyType {L: eqType} (E: Type) := {
my_l: L;
}.
HB.structure Definition My {L: eqType} := { E of MyType L E}.
Inductive foo_type := foo_singleton.
Canonical foo_eqType := EqType foo_type gen_eqMixin.
Canonical foo_choiceType := ChoiceType foo_type gen_choiceMixin.
Check MyType.Build _ _. (* looks ok *)
HB.instance Definition My_nat := MyType.Build foo_type nat.
(notice that replacing foo_type by foo_eqType in the last line gives another error message I don't get either).
Enrico Tassi (Oct 17 2022 at 12:39):You can't mix the old hand made hierarchy.
If you are based on https://github.com/math-comp/math-comp/pull/733 then you can probably do something along these lines, maybe look at ssralg and the module structure
Julien Puydt (Oct 17 2022 at 12:45):I'm not based on this ; I'm using the last released version.
Enrico Tassi (Oct 17 2022 at 13:11):If it is just an experiment, then copy/paste for that PR the mixin/structure for eqType, and so as for modules (which have a parameter which is another structure)
Julien Puydt (Oct 17 2022 at 13:20):@Enrico Tassi I sometimes get the impression that now isn't a particularly good time to try to dig into mathcomp: it's evolving pretty fast... on the other hand, that's also probably the best moment to make suggestions for the same reason...
Julien Puydt (Oct 24 2022 at 19:22):@Enrico Tassi nope, couldn't make it fly
Julien Puydt (Oct 27 2022 at 06:20):Here is what I tried to do to get HB-enabled eqType:
(* this comes from MC's git because I need HB-enabled eqType *)
Require Import ssrbool.
From HB Require Import structures.
Definition eq_axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
HB.mixin Record HasDecEq T := { eq_op : rel T; eqP : eq_axiom eq_op }.
and the last line fails because eq_op has type rel T while Type was expected... but rel comes from Coq's ssrbool, so it's again a case of mixed HB/non-HB, isn't it?
Enrico Tassi (Oct 27 2022 at 06:34):maybe eq_axiom does not have the right implicits? look like you are passing eq_op as the first and not second argument
Julien Puydt (Oct 27 2022 at 06:41):Oh dear, writing {T} instead of T in eq_axiom's definition indeed gives a better result... thanks!
Julien Puydt (Oct 27 2022 at 06:42):btw in the following lines:
#[mathcomp(axiom="eq_axiom"), short(type="eqType")]
HB.structure Definition Equality := { T of HasDecEq T }.
what does the first one do?
Enrico Tassi (Oct 27 2022 at 08:52):Here: https://github.com/math-comp/hierarchy-builder/blob/6598dc82ec9f9070bcea39fe5520c64fb7ec93d3/structures.v#L538-L594
(although mathcomp.axiom is not properly documented)
Julien Puydt (Oct 27 2022 at 09:07):Nice
Paolo Giarrusso (Oct 27 2022 at 09:55):Seems you needed {T} because you're not using the Set Implicit Arguments dance.
Julien Puydt (Oct 27 2022 at 14:43):I added the three lines:
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
to many of my lines.
I think I'm out of this hurdle: thanks!
Notification Bot (Oct 27 2022 at 14:43):Julien Puydt has marked this topic as resolved.
Last updated: May 28 2023 at 18:29 UTC