Ssreflect Users Discussion List

[Laurent Thery <>]

Hi,

Phantom is just a trick to let Coq infer the canonical structure 
automatically. In your example

Variable s1: set [eqType of nat].

would have worked.

The following seems to work in 8.5:

From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Nonrecursive Elimination Schemes.

Section SeqSet.

Variable T: eqType.

Record set :=
{
_set_seq :> seq T ;
_ : uniq _set_seq (* uniqueness property*)
}.

Canonical Structure setSubType := [subType for _set_seq by set_rect].
Definition set_eqMixin := [eqMixin of set by <:].
Canonical Structure mySubType_eqType := EqType set set_eqMixin.
Definition set_of of phant T := set.

End SeqSet.

Notation " '{set R } " := (set_of (Phant R)).

Variable s1: '{set nat}.