diff options
| author |  monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-25 16:02:04 +0000 |
|---|---|---|
| committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-25 16:02:04 +0000 |
| commit | 80567c19f2f44e7d244821039eb62a9a165dd440 (patch) | |
| tree | df223bf299baa157652a2bb98435ec2cbe6f2acb /ide | |
| parent | f8bbe83681d1de091a148578971e34a394728a56 (diff) | |
new utf8.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3953 85f007b7-540e-0410-9357-904b9bb8a0f7
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).*) |