5.7 Syntax facilities

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.2

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.3

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:
  1. 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.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.0.6.html at 8/10/98