Ssreflect Users Discussion List

[Felipe Cerqueira <>]

Hi Laurent,

Thank you, that worked nicely.
But I still have an issue. Could you try that in your machine?

  Variable s1: {set nat}.
  Check (1 \in s1).

Here I get the following error:
  The term "s1" has type "{setnat}" while it is expected to have type 
"pred_sort ?5".

I usually get this kind of error when I forget to declare the canonical 
structure with eqType.
Do you know what happened in this case?


Thanks,
Felipe

On 4/21/16 1:21 PM, Laurent Thery wrote:
> 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}.