Syntax and Notations
(Part of the Coq FAQ)
You can define your own notation for forall:
Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).or if your are using CoqIde you can define a pretty symbol for forall and an input method (see this section).
You can use for instance:
Require Import Coq.Reals.Rdefinitions.
Notation "x ^ 2" := (Rmult x x) (at level 20).Note that you can not use:
Notation "x2" := (Rmult x x) (at level 20).
because “2” is an iso-latin character. If you really want this kind of notation you should use UTF-8.
Because we rely on Camlp4 for syntactical analysis and Camlp4 does not really implement no associativity. By default, non-associative operators are defined as right-associative.
You can do “Print Grammar constr”, and decode the output from Camlp4, good luck!
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.