21 lines
458 B
Coq
21 lines
458 B
Coq
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Type.20class.20constraint.20in.20record.20type.20member *)
|
|
|
|
Inductive myBool: Type := mtrue | mfalse.
|
|
|
|
Class Eq (A: Type) := {
|
|
eqbC: A -> A -> bool
|
|
}.
|
|
|
|
#[export] Instance eqmBool : Eq myBool := {
|
|
eqbC := fun x y =>
|
|
match x, y with
|
|
| mtrue, mtrue => true
|
|
| mfalse, mfalse => true
|
|
| _, _ => false
|
|
end
|
|
}.
|
|
|
|
Record myRec := {
|
|
eqElem {A: Type} `{Eq A}: A -> A -> bool
|
|
}.
|