Ssreflect Users Discussion List

[Emilio Jesús Gallego Arias <>]

Hi Bas,

Bas Spitters 
<>
 writes:

> Is there an established way to obtain an eqType on a Record?

TTBOMK the `newType` construction doesn't work for singleton inductives
that take more than one parameter, but I could be wrong.

Some manual meddling will get you there tho:

8<---------------------------------------------------------------------8<
From mathcomp Require Import all_ssreflect.

Record foo := { bar : nat; baz: bool }.

Definition of_foo f := (f.(bar), f.(baz)).
Definition to_foo '(bar,baz) := {| bar := bar; baz := baz |}.

Definition foo_sub : @subType (nat*bool) xpredT.
apply: (@NewType _ _ of_foo to_foo); last by case.
by move=> P K [bar baz]; have := K (bar, baz).
Defined.

Canonical foo_subType := Eval hnf in foo_sub.
Canonical foo_eqType  := Eval hnf in EqType _ [eqMixin of foo by <: ].
8<---------------------------------------------------------------------8<

I guess that it would be worth to improve the heuristic so it works out
of the box.

E.