Commit ca6ea63a authored by Robbert Krebbers's avatar Robbert Krebbers

Notation `⊑@{A}`.

parent 08ce9e37
......@@ -1204,6 +1204,10 @@ 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 ().
Hint Extern 0 (_ _) => reflexivity.
......
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