From ddfcc76cd4b43557ccef390077e209a58dee3a4f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Feb 2020 09:59:43 +0100
Subject: [PATCH] Move lattice related stuff up.

---
 theories/base.v | 85 +++++++++++++++++++++++++------------------------
 1 file changed, 43 insertions(+), 42 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 30feccb2..bb1a5d5b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1158,6 +1158,49 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
 Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 
+(** * Notations for lattices. *)
+(** SqSubsetEq registers the "canonical" partial order for a type, and is used
+for the \sqsubseteq symbol. *)
+Class SqSubsetEq A := sqsubseteq: relation A.
+Hint Mode SqSubsetEq ! : typeclass_instances.
+Instance: Params (@sqsubseteq) 2 := {}.
+Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
+Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
+Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
+Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
+
+Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
+Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
+
+Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+
+Hint Extern 0 (_ ⊑ _) => reflexivity : core.
+
+Class Meet A := meet: A → A → A.
+Hint Mode Meet ! : typeclass_instances.
+Instance: Params (@meet) 2 := {}.
+Infix "⊓" := meet (at level 40) : stdpp_scope.
+Notation "(⊓)" := meet (only parsing) : stdpp_scope.
+Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
+Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
+
+Class Join A := join: A → A → A.
+Hint Mode Join ! : typeclass_instances.
+Instance: Params (@join) 2 := {}.
+Infix "⊔" := join (at level 50) : stdpp_scope.
+Notation "(⊔)" := join (only parsing) : stdpp_scope.
+Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
+Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
+
+Class Top A := top : A.
+Hint Mode Top ! : typeclass_instances.
+Notation "⊤" := top (format "⊤") : stdpp_scope.
+
+Class Bottom A := bottom : A.
+Hint Mode Bottom ! : typeclass_instances.
+Notation "⊥" := bottom (format "⊥") : stdpp_scope.
+
+
 (** * Axiomatization of sets *)
 (** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
 elements of type [A]. The first class, [SemiSet] does not include intersection
@@ -1276,45 +1319,3 @@ Class Half A := half: A → A.
 Hint Mode Half ! : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
-
-(** * Notations for lattices. *)
-(** SqSubsetEq registers the "canonical" partial order for a type, and is used
-for the \sqsubseteq symbol. *)
-Class SqSubsetEq A := sqsubseteq: relation A.
-Hint Mode SqSubsetEq ! : typeclass_instances.
-Instance: Params (@sqsubseteq) 2 := {}.
-Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
-Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
-Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
-Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
-
-Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
-Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
-
-Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
-
-Hint Extern 0 (_ ⊑ _) => reflexivity : core.
-
-Class Meet A := meet: A → A → A.
-Hint Mode Meet ! : typeclass_instances.
-Instance: Params (@meet) 2 := {}.
-Infix "⊓" := meet (at level 40) : stdpp_scope.
-Notation "(⊓)" := meet (only parsing) : stdpp_scope.
-Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
-Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
-
-Class Join A := join: A → A → A.
-Hint Mode Join ! : typeclass_instances.
-Instance: Params (@join) 2 := {}.
-Infix "⊔" := join (at level 50) : stdpp_scope.
-Notation "(⊔)" := join (only parsing) : stdpp_scope.
-Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
-Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
-
-Class Top A := top : A.
-Hint Mode Top ! : typeclass_instances.
-Notation "⊤" := top (format "⊤") : stdpp_scope.
-
-Class Bottom A := bottom : A.
-Hint Mode Bottom ! : typeclass_instances.
-Notation "⊥" := bottom (format "⊥") : stdpp_scope.
-- 
GitLab