Commit 0ee40447 authored by Robbert Krebbers's avatar Robbert Krebbers

More consistent notations for curried relations.

For example, instead of:

  Notation "( X ⊆ )"

We now use:

  Notation "( X ⊆)"

We were already doing this for = and ≡.

This solves some conflicts with the notations of MetaCoq.
parent e8e97884
Pipeline #3938 passed with stage
in 5 minutes and 19 seconds
......@@ -642,12 +642,12 @@ Class SubsetEq A := subseteq: relation A.
Instance: Params (@subseteq) 2.
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
Notation "( X ⊆ )" := (subseteq X) (only parsing) : C_scope.
Notation "( ⊆ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : C_scope.
Notation "(⊆ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "X ⊈ Y" := (¬X Y) (at level 70) : C_scope.
Notation "(⊈)" := (λ X Y, X Y) (only parsing) : C_scope.
Notation "( X ⊈ )" := (λ Y, X Y) (only parsing) : C_scope.
Notation "( ⊈ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "( X ⊈)" := (λ Y, X Y) (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.
......@@ -662,12 +662,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity.
Infix "⊂" := (strict ()) (at level 70) : C_scope.
Notation "(⊂)" := (strict ()) (only parsing) : C_scope.
Notation "( X ⊂ )" := (strict () X) (only parsing) : C_scope.
Notation "( ⊂ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "X ⊄ Y" := (¬X Y) (at level 70) : C_scope.
Notation "( X ⊂)" := (strict () X) (only parsing) : C_scope.
Notation "(⊂ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "X ⊄ Y" := (¬X Y) (at level 70) : C_scope.
Notation "(⊄)" := (λ X Y, X Y) (only parsing) : C_scope.
Notation "( X ⊄ )" := (λ Y, X Y) (only parsing) : C_scope.
Notation "( ⊄ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "( X ⊄)" := (λ Y, X Y) (only parsing) : C_scope.
Notation "(⊄ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "X ⊆ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : C_scope.
Notation "X ⊆ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : C_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