Is it possible to have a type class constraint in a member of a record type?

Like:

```
Inductive myBool: Type := mtrue | mfalse.
Class Eq (A: Type) := {
eqbC: A -> A -> bool
}.
Instance eqmBool : Eq myBool := {
eqbC := fun x y =>
match x, y with
| mtrue, mtrue => true
| mfalse, mfalse => true
| _, _ => false
end
}.
Record myRec := {
eqElem: A `{Eq A} (* Something like this possible? *)
}.
```

You can write `eqElem : Eq A -> A`

, and maybe even

```
eqElem `{Eq A} : A
```

Last updated: Jun 23 2024 at 05:02 UTC