Ssreflect Users Discussion List

[Felipe Cerqueira <>]

Hello,

I was trying to build a simple ListSet in ssreflect on top of seq, as opposed to using finsets (since they only work with fintypes).
I'm used to working with seq, so it would be nice to have a "list that is uniq".
I tried the following code:

Section SeqSet.

  Context {T: eqType}.

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

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

End SeqSet.
 
Even though the code above compiles, I'm not able to do the following:

  Variable s1: set nat.
  Variable s2: set 'I_10.

The problem is that nat is the Type, not the eqType.
I tried having a look at finset.v to see how it is done there, but there was something about
Phantom that I didn't understand.

Is there an easy way to do this? What I've been doing so far is to use lists everywhere
and add the hypothesis of uniqueness separately.

Thanks,
Felipe