So I have a canonical structure as follows:
Structure serDe := Pack{
CST: Type;
ops: operations CST;
lms: lemmas ops;
}.
and then there eqType
and I am trying to specify types that implement both serDe + eqType
so I had:
Module SerDeEqType.
Record mixin T := Mixin {
Eq_type: Equality.mixin_of T;
SerDe_ops: SerDe.operations T;
SerDe_lemmas: SerDe.lemmas SerDe_ops;
}.
Record type := Class {
SEQ: Type;
ops: mixin SEQ;
}.
Definition to_eq (t: type) : eqType :=
Equality.Pack (Eq_type (SEQ t) (ops t)).
Definition to_serde (t: type) : serDe :=
SerDe.Pack (SerDe_lemmas (SEQ t) (ops t)).
End SerDeEqType.
Canonical Structure SerDeEqType.to_eq.
Canonical Structure SerDeEqType.to_serde.
But the problem is I still need to manually implement SerDeEqType.type
for every type that implements both CS, I tried thinking of way of doing it automatically, but it didn't work. What would be the mathcomp idomatic way of handling this problem?
Hi, the modern answer to that problem is https://github.com/math-comp/hierarchy-builder
Unfortunaltely to work properly with eqType you need to wait for the next major release of mathcomp...
An alpha release is scheduled for Christmas
(really)
alright, here is a question,
Scared of making your project depend on HB? This section is for you.
so what make you think that people would think that depending on HB is problem in this particular when compared to other coq code ?
also does that mean that mathcomp will also depend on HB ?
Yeah I think that's the plan for 2.0
walker said:
alright, here is a question,
Scared of making your project depend on HB? This section is for you.
so what make you think that people would think that depending on HB is problem in this particular when compared to other coq code ?
It is not specific to HB or Coq either. People who wants to build a project in the long term do look at what they depend on. This is not always the case for research projects, but sometimes it is. And it is also subjective, some people buy stock options some other don't ;-)
I think that explaining what HB commands do in terms of regular Coq commands is reassuring for a non negligible class of users, this is what that documentation section is about
On a side note, the fact that we can run MC 2.0 + HB + ... in the browser is quite reassuring for me, e.g. it will make my teaching life a lot easier. I would not have bet on this one year ago. [I'm still working on that page, it may be broken from time to time].
There are many aspects to be considered, and "how hard will it be for students to run it" is one of them.
Cyril Cohen said:
Hi, the modern answer to that problem is https://github.com/math-comp/hierarchy-builder
Unfortunaltely to work properly with eqType you need to wait for the next major release of mathcomp...
What do you mean by to work properly? So far I've been under the impression that eqType
works properly, at least in some senses. In what sense does eqType
doesn't work properly?
Last updated: Apr 17 2024 at 19:01 UTC