5.7 Syntax facilities
We present quickly in this section some syntactic facilities.
We will only sketch them here and refer the
interested reader to chapter 9 for more details and
examples.
5.7.1 Implicit Arguments [ On | Off ].
These commands sets and unsets the implicit argument mode. This mode
forces not explicitly give some arguments (typically type arguments in
polymorphic functions) which are deductible from the other arguments.
See also: section 2.6.1
5.7.2 Syntactic Definition ident := term.
This command defines ident as an
abbreviation with implicit arguments. Implicit arguments are denoted
in term by ? and they will have to be synthesized by the
system.
Remark: Since it may contain don't care variables ?, the argument
term cannot be typechecked at
definition time. But each of its subsequent usages will be.
See also: section 2.6.2
5.7.3 Syntax ident syntax-rules.
This command addresses the extensible
pretty-printing mechanism of Coq. It allows ident2 to be
pretty-printed as specified in syntax-rules. Many examples
of the Syntax command usage may be found in the PreludeSyntax file (see directory $COQLIB/theories/INIT).
See also: chapter 9
5.7.4 Grammar ident1 ident2 := grammar-rule.
This command allows to give explicitly new grammar rules for parsing
the user's own notation. It may be used instead of the Syntactic
Definition pragma. It can also be used by an advanced Coq's user
who programs his own tactics.
See also: chapters 9,
10
5.7.5 Infix num string ident.
This command declares a prefix operator ident as infix, with the
syntax term string term. num is the precedence associated to
the operator; it must lie between 1 and 10. The infix operator string
associates to the left. string must be a legal token. Both grammar
and pretty-print rules are automatically generated for string.
Variants:
-
Infix assoc num string ident.
Declares ident as an infix operator with an alternate
associativity. assoc may be one of LEFTA, RIGHTA and NONA. The default is LEFTA. When an
associativity is given, the precedence level must lie between 6 and
9.