Stream: Coq users

Topic: Type class constraint in record type member


view this post on Zulip Julin Shaji (Jan 01 2024 at 07:20):

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? *)
}.

view this post on Zulip Paolo Giarrusso (Jan 01 2024 at 11:13):

You can write eqElem : Eq A -> A, and maybe even

eqElem `{Eq A} : A

Last updated: Jun 23 2024 at 05:02 UTC