diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 9455228e7d..8b7fe20191 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -230,10 +230,12 @@ mathematical symbols ∀ and ∃, you may define: .. coqtop:: in - Notation "∀ x : T, P" := - (forall x : T, P) (at level 200, x ident). - Notation "∃ x : T, P" := - (exists x : T, P) (at level 200, x ident). + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. + Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by |