Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]


(** In this section, we define a notion of a set (based on a sequence
    without duplicates). *)
Section SeqSet.

  (** Let [T] be any type with decidable equality. *)
  Context {T : eqType}.

  (** We define a set as a sequence that has no duplicates. *)
  Record set :=
  {
    _set_seq :> seq T ;
    _ : uniq _set_seq (* no duplicates *)
  }.

  (** Now we add the [ssreflect] boilerplate code to support [_ == _]
      and [_ ∈ _] operations. *)
  Canonical Structure setSubType := [subType for _set_seq].
  Definition set_eqMixin := [eqMixin of set by <:].
  Canonical Structure set_eqType := EqType set set_eqMixin.
  
Ignoring canonical projection to mem_seq by topred in
mem_set_predType: redundant with mem_seq_predType
[redundant-canonical-projection,typechecker]

  Definition set_of of phant T := set.


Ignoring canonical projection to mem_seq by topred in
@mem_set_predType: redundant with mem_seq_predType
[redundant-canonical-projection,typechecker]


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

(** Next we prove a basic lemma about sets. *)
Section Lemmas.

  (** Consider a set [s]. *)
  Context {T : eqType}.
  Variable s : {set T}.

  (** Then we show that element of [s] are unique. *)
  
T: eqType
s: {setT}
uniq s

  
T: eqType
s: {setT}
uniq s
 by destruct s. Qed.

End Lemmas.