From ad870687cd82833a3995b19bea4c27e04c16b8f8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 00:31:28 +0100
Subject: [PATCH] =?UTF-8?q?Type=20class=20for=20=E2=8A=A4=20to=20get=20ove?=
 =?UTF-8?q?rloaded=20notation=20for=20entire=20set.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v    | 5 ++++-
 theories/bsets.v   | 2 +-
 theories/co_pset.v | 2 +-
 theories/sets.v    | 2 +-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 4452a696..08e1f021 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -209,6 +209,9 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
+Class Top A := top : A.
+Notation "⊤" := top : C_scope.
+
 Class Union A := union: A → A → A.
 Instance: Params (@union) 2.
 Infix "∪" := union (at level 50, left associativity) : C_scope.
@@ -311,7 +314,7 @@ Instance: Params (@disjoint) 2.
 Infix "⊥" := disjoint (at level 70) : C_scope.
 Notation "(⊥)" := disjoint (only parsing) : C_scope.
 Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
-Notation "(.⊥ X )" := (λ Y, Y ⊥  X) (only parsing) : C_scope.
+Notation "(.⊥ X )" := (λ Y, Y ⊥ X) (only parsing) : C_scope.
 Infix "⊥*" := (Forall2 (⊥)) (at level 70) : C_scope.
 Notation "(⊥*)" := (Forall2 (⊥)) (only parsing) : C_scope.
 Infix "⊥**" := (Forall2 (⊥*)) (at level 70) : C_scope.
diff --git a/theories/bsets.v b/theories/bsets.v
index 8ae132f1..2b486081 100644
--- a/theories/bsets.v
+++ b/theories/bsets.v
@@ -6,7 +6,7 @@ From stdpp Require Export prelude.
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
 Arguments mkBSet {_} _.
 Arguments bset_car {_} _ _.
-Definition bset_all {A} : bset A := mkBSet (λ _, true).
+Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
 Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
 Instance bset_singleton {A} `{∀ x y : A, Decision (x = y)} :
   Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
diff --git a/theories/co_pset.v b/theories/co_pset.v
index 85e80a46..16692659 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -148,7 +148,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
   coPset_singleton_raw p ↾ coPset_singleton_wf _.
 Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
 Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Definition coPset_all : coPset := coPLeaf true ↾ I.
+Instance coPset_top : Top coPset := coPLeaf true ↾ I.
 Instance coPset_union : Union coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
diff --git a/theories/sets.v b/theories/sets.v
index bb9c9ddd..a6740fab 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -6,7 +6,7 @@ From stdpp Require Export prelude.
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Arguments mkSet {_} _.
 Arguments set_car {_} _ _.
-Definition set_all {A} : set A := mkSet (λ _, True).
+Instance set_all {A} : Top (set A) := mkSet (λ _, True).
 Instance set_empty {A} : Empty (set A) := mkSet (λ _, False).
 Instance set_singleton {A} : Singleton A (set A) := λ x, mkSet (x =).
 Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
-- 
GitLab