Stream: Coq users

Topic: ✔ Type class constraint in record type member


view this post on Zulip Julin Shaji (Jan 02 2024 at 07:42):

Thanks!

Record myRec := {
  eqElem {A: Type} `{Eq A}: A -> A -> bool
}.

worked.

Though I guess having it as a separate function would probably be better than having it in a record.

view this post on Zulip Notification Bot (Jan 02 2024 at 07:42):

Julin Shaji has marked this topic as resolved.


Last updated: Jun 13 2024 at 19:02 UTC