diff options
| author | monate | 2003-04-25 16:02:04 +0000 |
|---|---|---|
| committer | monate | 2003-04-25 16:02:04 +0000 |
| commit | 80567c19f2f44e7d244821039eb62a9a165dd440 (patch) | |
| tree | df223bf299baa157652a2bb98435ec2cbe6f2acb | |
| parent | f8bbe83681d1de091a148578971e34a394728a56 (diff) | |
new utf8.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3953 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | INSTALL.ide | 2 | ||||
| -rw-r--r-- | ide/utf8.v | 21 |
2 files changed, 20 insertions, 3 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index 7e08a23724..6e471348e0 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -44,7 +44,7 @@ INSTALLATION cd /tmp && \ wget http://www.lri.fr/~monate/download/lablgtk2-coqide.tgz && \ tar zxvf lablgtk2-coqide.tgz && \ - cd lablgtk2 && \ + cd lablgtk2-coqide && \ make configure && \ make all opt && \ make install diff --git a/ide/utf8.v b/ide/utf8.v index d0d94dc518..6b32a559c6 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).*) |