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 Set Implicit Arguments.
This command sets the implicit argument mode on. Under this mode, the
arguments of declared constructions (constants, inductive types,
variables, ...) which can automatically be deduced from the others
arguments (typically type arguments in polymorphic functions) are
skipped. They are not printed and the user must not give them. To
show what are the implicit arguments associated to a declaration
qualid, use Print qualid. You can change the implicit
arguments of a specific declaration by using the command
Implicits (see section 5.7.2). You can explicitely
give an argument which otherwise should be implicit by using the
symbol !
(see section 2.7.1).
To set the implicit argument mode off, use Unset Implicit Arguments.
Variants:
-
Implicit Arguments On.
This is a deprecated equivalent to Set Implicit Arguments.
- Implicit Arguments Off.
This is a deprecated equivalent to Unset Implicit Arguments.
See also: section 2.7.1
5.7.2 Implicits qualid [
num1 ...numn ]
This sets the implicit arguments of reference qualid to be the
arguments at positions num1 ...numn. As a particular
case, if the list of numbers is empty then no implicit argument is
associated to qualid.
5.7.3 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.7.2
5.7.4 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.5 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
5.7.6 Infix num string qualid.
This command declares the prefix operator denoted by qualid 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 qualid.
Declares the full names denoted by qualid 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.