ajout d'un debut de proprietes pour les FSetWeak

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 8 deletions

diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 2cf5d5d22..598a75924 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -38,7 +38,18 @@ Module Type S.
   Definition elt := E.t.
 
   Parameter t : Set. (** the abstract type of sets *)
- 
+
+  (** Logical predicates *)
+  Parameter In : elt -> t -> Prop.
+  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+  
+  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
+  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
+
   Parameter empty : t.
   (** The empty set. *)
 
@@ -124,13 +135,6 @@ Module Type S.
   Variable s s' s'' : t.
   Variable x y z : elt.
 
-  Parameter In : elt -> t -> Prop.
-  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
-  Definition Subset s s' := forall a : elt, In a s -> In a s'.
-  Definition Empty s := forall a : elt, ~ In a s.
-  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
-  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
-
   (** Specification of [In] *)
   Parameter In_1 : E.eq x y -> In x s -> In y s.