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.

What is `Sortclass`

and how is it different to `Type`

?

`Sortclass`

is a class and `Type`

is a type.

@Jordan Mitchell Barrett here is the relevant section of the coq documentation https://coq.inria.fr/refman/addendum/implicit-coercions.html#classes

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.

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: Jun 20 2024 at 13:02 UTC