So the sinnet I am struggling with is something similar to this:

```
From mathcomp Require Import all_ssreflect.
Section FOO.
Context {A B: Type}.
Context {eqA: A -> A -> bool}.
Context {eqAP: Equality.axiom eqA}.
Context `{!EqType A (EqMixin eqAP)}.
Lemma foo: forall (a: A) (acc: seq A),
a \in acc.
Admitted.
End FOO.
```

the error message does not make sense:

```
The term "acc" has type "seq A" while it is expected to have type
"pred_sort ?pT".
```

When I try to replace `A`

with `nat`

, everything works flawlessly, that means the problem is with `A`

and not with `seq`

`eqType`

is noi a typeclass, what you wrote does not work in the current state of affairs.

Here is the context that makes it work:

```
From mathcomp Require Import all_ssreflect.
Section FOO.
Context {A : eqType}.
Lemma foo: forall (a: A) (acc: seq A), a \in acc.
Admitted.
End FOO.
```

pardon me!

I am struggling to understand how this work given that line:

https://math-comp.github.io/htmldoc/mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType

What is the difference between

```
Context {A : eqType}.
```

and

```
Context {A : Type}.
```

`Context {A : eqType}.`

introduces an element of a structure (`eqType`

) which contains a `Type`

(accessible though a coercion, hence you can write `x : A`

and Coq will automatically understand `x : Equality.sort`

);, an operator (`==`

) and a proof that this equality is "the same" as `=`

, but as a boolean.

:+1: given your link, I wonder if I should point out that `type`

is https://math-comp.github.io/htmldoc/mathcomp.ssreflect.eqtype.html#Equality.type

I misread `type`

as `Type`

thanks everyone!

and I'm tempted to recommend https://hal.inria.fr/hal-00816703v1/document to see a quick introduction to canonical structures and their use in math-comp

Also https://zenodo.org/record/7118596#.Y1fwAUpBy8Q part 2 should help (but is longer)

Last updated: Jul 15 2024 at 21:02 UTC