diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/utf8.v | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/ide/utf8.v b/ide/utf8.v index d0d94dc51..6b32a559c 100644 --- a/ide/utf8.v +++ b/ide/utf8.v @@ -1,2 +1,19 @@ -Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10). -Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10). +(* Logic *) +Notation "∀ x : t , P" := (x:t)P (at level 1, x,t,P at level 10). +Notation "∃ x : t , P" := (EXT x:t|P) (at level 1, x,t,P at level 10). +Notation "x ∨ y" := (x \/ y) (at level 1, y at level 10). +Notation "x ∧ y" := (x /\ y) (at level 1, y at level 10). +Notation "x ⇒ y" := (x -> y) (at level 1, y at level 10). +Notation "x ⇔ y" := (x <-> y) (at level 1, y at level 10). +Notation "⌉ x" := (~x) (at level 1, x at level 10). + +(* Abstraction *) +Notation "'λ' x : T , y" := ([x:T] y) (at level 1, x,T,y at level 10). +Notation "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10). + +(* Arithmetic *) +Notation "x ≤ y" := (le x y) (at level 3, y at level 10). +Notation "x ≥ y" := (ge x y) (at level 3, y at level 10). + +(* Require ZArith. + Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10).*) |