Commit ee274b1c authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Empty body for RewriteRelation instance.

parent 2c8e0d69
......@@ -47,7 +47,7 @@ Infix "⊏1*" := (Forall2 (λ p q, p.1 ⊏ q.1)) (at level 70) : stdpp_scope.
Infix "⊏2*" := (Forall2 (λ p q, p.2 q.2)) (at level 70) : stdpp_scope.
Infix "⊏1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : stdpp_scope.
Infix "⊏2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : stdpp_scope.
Instance Strict_sqsubseteq_Rewrite `{SqSubsetEq T} : @RewriteRelation T ().
Instance Strict_sqsubseteq_Rewrite `{SqSubsetEq T} : @RewriteRelation T () := {}.
Infix "⊔*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope.
Notation "(⊔*)" := (zip_with ()) (only parsing) : stdpp_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment