Jordan Mitchell Barrett (Apr 02 2021 at 06:33): Jordan Mitchell Barrett (Apr 02 2021 at 06:33):Why does Coq reject the following?
Inductive metricspace :=
| met (X:Type)(d: X -> X -> R)`{is_metric d}.
Definition MStoT (M:metricspace) :=
match M with
| met X d => X
end.
Coercion MStoT : metricspace >-> Type.
Syntax error: [class_rawexpr] expected after '>->' (in [gallina_ext]).
As the message says, Type is not a class. Try with, e.g., Sortclass instead.
Jordan Mitchell Barrett (Apr 02 2021 at 06:43):What is Sortclass and how is it different to Type?
Guillaume Melquiond (Apr 02 2021 at 06:43):Sortclass is a class and Type is a type.
Cyril Cohen (Apr 02 2021 at 07:34):@Jordan Mitchell Barrett here is the relevant section of the coq documentation https://coq.inria.fr/refman/addendum/implicit-coercions.html#classes
Jordan Mitchell Barrett (Apr 02 2021 at 09:56):Thanks @Guillaume Melquiond and @Cyril Cohen. Speaking of coercions, is it possible to make proj1_sig a coercion for any A : Type, P : A -> Prop? I tried
Coercion sig1co {A : Type}{P : A -> Prop}(y:{x : A | P x}) := proj1_sig y.
but Coq didn't like it.
Matthieu Sozeau (Apr 02 2021 at 10:31):The coercion system does not accept such "generic" coercions, but if you use Program it implements this coercion (and the converse, generating a proof obligation when you implicitely inject in a subset type). Be sure to Unset Program Cases so that your matches and lets don't get interpreted by program unless you really want to https://coq.inria.fr/refman/addendum/program.html?highlight=program#coq:flag.Program-Cases
Last updated: Oct 13 2024 at 01:02 UTC