sqsubseteq is a RewriteRelation.

9a5be071 · Jacques-Henri Jourdan · fd3ed134 · 9a5be071
Commit 9a5be071 authored Dec 04, 2017 by Jacques-Henri Jourdan
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

theories/base.v theories/base.v +1 -0

No files found.
--- a/theories/base.v
+++ b/theories/base.v
@@ -1125,6 +1125,7 @@ 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.
+Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).

 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.