Chapter 11 Syntax extensions and interpretation scopes
In this chapter, we introduce advanced commands to modify the way
Coq parses and prints objects, i.e. the translations between the
concrete and internal representations of terms and commands. The main
commands are Notation and Infix which are described in
section 11.1. It also happens that the same symbolic
notation is expected in different contexts. To achieve this form of
overloading, Coq offers a notion of interpretation scope. This is
described in section 11.2.
Remark: The commands Grammar, Syntax and Distfix which
were present for a while in Coq are no longer available from Coq
version 8.0. The underlying AST structure is also no longer available.
The functionalities of the command Syntactic Definition are
still available, see section 11.3.
11.1 Notations
11.1.1 Basic notations
A notation is a symbolic abbreviation denoting some term
or term pattern.
A typical notation is the use of the infix symbol /\ to denote
the logical conjunction (and). Such a notation is declared
by
Coq < Notation "A /\ B" := (and A B).
The expression (and A B) is the abbreviated term and the
string "A /\ B" (called a notation) tells how it is
symbolically written.
A notation is always surrounded by double quotes (excepted when the
abbreviation is a single ident, see 11.3). The
notation is composed of tokens separated by spaces. Identifiers
in the string (such as A and B) are the parameters of the notation. They must occur at least once each in the
denoted term. The other elements of the string (such as /\) are
the symbols.
An identifier can be used as a symbol but it must be surrounded by
simple quotes to avoid the confusion with a parameter. Similarly,
every symbol of at least 3 characters and starting with a simple quote
must be quoted (then it starts by two single quotes). Here is an example.
Coq < Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
A notation binds a syntactic expression to a term. Unless the parser
and pretty-printer of Coq already know how to deal with the
syntactic expression (see 11.1.7), explicit precedences and
associativity rules have to be given.
11.1.2 Precedences and associativity
Mixing different symbolic notations in a same text may cause serious
parsing ambiguity. To deal with the ambiguity of notations, Coq
uses precedence levels ranging from 0 to 100 (plus one extra level
numbered 200) and associativity rules.
Consider for example the new notation
Coq < Notation "A \/ B" := (or A B).
Clearly, an expression such as (A:Prop)True /\ A \/
A \/ False is ambiguous. To tell the Coq parser how to
interpret the expression, a priority between the symbols /\ and
\/ has to be given. Assume for instance that we want conjunction
to bind more than disjunction. This is expressed by assigning a
precedence level to each notation, knowing that a lower level binds
more than a higher level. Hence the level for disjunction must be
higher than the level for conjunction.
Since connectives are the less tight articulation points of a text, it
is reasonable to choose levels not so far from the higher level which
is 100, for example 85 for disjunction and 80 for
conjunction1.
Similarly, an associativity is needed to decide whether True /\
False /\ False defaults to True /\ (False
/\ False) (right associativity) or to (True
/\ False) /\ False (left associativity). We may
even consider that the expression is not well-formed and that
parentheses are mandatory (this is a ``no associativity'')2.
We don't know of a special convention of the associativity of
disjunction and conjunction, let's apply for instance a right
associativity (which is the choice of Coq).
Precedence levels and associativity rules of notations have to be
given between parentheses in a list of modifiers that the
Notation command understands. Here is how the previous
examples refine.
Coq < Notation "A /\ B" := (and A B) (at level 80, right associativity).
Coq < Notation "A \/ B" := (or A B) (at level 85, right associativity).
By default, a notation is considered non associative, but the
precedence level is mandatory (except for special cases whose level is
canonical). The level is either a number or the mention next
level whose meaning is obvious. The list of levels already assigned
is on Figure 3.1.
11.1.3 Complex notations
Notations can be made from arbitraly complex symbols. One can for
instance define prefix notations.
Coq < Notation "~ x" := (not x) (at level 75, right associativity).
One can also define notations for incomplete terms, with the hole
expected to be inferred at typing time.
Coq < Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
One can define closed notations whose both sides are symbols. In
this case, the default precedence level for inner subexpression is 200.
Coq < Notation "( x , y )" := (@pair _ _ x y) (at level 0).
One can also define notations for binders.
Coq < Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0).
In the last case though, there is a conflict with the notation for
type casts. This last notation, as shown by the command Print Grammar
constr is at level 100. To avoid x : A being parsed as a type cast,
it is necessary to put x at a level below 100, typically 99. Hence, a
correct definition is
Coq < Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99).
See the next section for more about factorisation.
11.1.4 Simple factorisation rules
Coq extensible parsing is performed by Camlp4 which is essentially a
LL1 parser. Hence, some care has to be taken not to hide already
existing rules by new rules. Some simple left factorisation work has
to be done. Here is an example.
Coq < Notation "x < y" := (lt x y) (at level 70).
Coq < Notation "x < y < z" := (x < y /\ y < z) (at level 70).
In order to factorise the left part of the rules, the subexpression
referred by y has to be at the same level in both rules. However
the default behavior puts y at the next level below 70
in the first rule (no associativity is the default), and at the level
200 in the second rule (level 200 is the default for inner expressions).
To fix this, we need to force the parsing level of y,
as follows.
Coq < Notation "x < y" := (lt x y) (at level 70).
Coq < Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
For the sake of factorisation with Coq predefined rules, simple
rules have to be observed for notations starting with a symbol:
e.g. rules starting with ``{'' or ``('' should be put at level 0. The
list of Coq predefined notations can be found in chapter 3.
The command to display the current state of the Coq term parser is
Print Grammar constr.
11.1.5 Displaying symbolic notations
The command Notation has an effect both on the Coq parser and
on the Coq printer. For example:
Coq < Check (and True True).
True /\ True
: Prop
However, printing, especially pretty-printing, requires
more care than parsing. We may want specific indentations,
line breaks, alignment if on several lines, etc.
The default printing of notations is very rudimentary. For printing a
notation, a formatting box is opened in such a way that if the
notation and its arguments cannot fit on a single line, a line break
is inserted before the symbols of the notation and the arguments on
the next lines are aligned with the argument on the first line.
A first, simple control that a user can have on the printing of a
notation is the insertion of spaces at some places of the
notation. This is performed by adding extra spaces between the symbols
and parameters: each extra space (other than the single space needed
to separate the components) is interpreted as a space to be inserted
by the printer. Here is an example showing how to add spaces around
the bar of the notation.
Coq < Notation "{{ x : A | P }}" := (sig (fun x : A => P))
Coq < (at level 0, x at level 99).
Coq < Check (sig (fun x : nat => x=x)).
{{x : nat | x = x}}
: Set
The second, more powerful control on printing is by using the format modifier. Here is an example
Coq < Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
Coq < (at level 200, right associativity, format
Coq < "'[v ' 'If' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'").
Defining 'If' as keyword
A format is an extension of the string denoting the notation with
the possible following elements delimited by single quotes:
-
extra spaces are translated into simple spaces
- tokens of the form
'/ ' are translated into breaking point,
in case a line break occurs, an indentation of the number of spaces
after the ``/'' is applied (2 spaces in the given example)
- token of the form
'//' force writing on a new line
- well-bracketed pairs of tokens of the form
'[ ' and ']'
are translated into printing boxes; in case a line break occurs,
an extra indentation of the number of spaces given after the ``[''
is applied (4 spaces in the example)
- well-bracketed pairs of tokens of the form
'[hv ' and ']'
are translated into horizontal-orelse-vertical printing boxes;
if the content of the box does not fit on a single line, then every breaking
point forces a newline and an extra indentation of the number of spaces
given after the ``['' is applied at the beginning of each newline
(3 spaces in the example)
- well-bracketed pairs of tokens of the form
'[v ' and
']' are translated into vertical printing boxes; every
breaking point forces a newline, even if the line is large enough to
display the whole content of the box, and an extra indentation of the
number of spaces given after the ``['' is applied at the beginning
of each newline
Thus, for the previous example, we get
Notations do not survive the end of sections. No typing of the denoted
expression is performed at definition time. Type-checking is done only
at the time of use of the notation.
Coq < Check
Coq < (IF_then_else (IF_then_else True False True)
Coq < (IF_then_else True False True)
Coq < (IF_then_else True False True)).
If If True
then False
else True
then If True
then False
else True
else If True
then False
else True
: Prop
Remark: Sometimes, a notation is expected only for the parser.
To do so, the option only parsing is allowed in the list of modifiers of
Notation.
11.1.6 The Infix command
The Infix command is a shortening for declaring notations of
infix symbols. Its syntax is
Infix "symbol" := qualid ( modifier , ... , modifier ).
and it is equivalent to
Notation "x symbol y" := (qualid x y) ( modifier , ... , modifier ).
where x and y are fresh names distinct from qualid. Here is an example.
Coq < Infix "/\" := and (at level 80, right associativity).
11.1.7 Reserving notations
A given notation may be used in different contexts. Coq expects all
uses of the notation to be defined at the same precedence and with the
same associativity. To avoid giving the precedence and associativity
every time, it is possible to declare a parsing rule in advance
without giving its interpretation. Here is an example from the initial
state of Coq.
Coq < Reserved Notation "x = y" (at level 70, no associativity).
Reserving a notation is also useful for simultaneously defined an
inductive type or a recursive constant and a notation for it.
Remark: The notations mentioned on Figure 3.1 are
reserved. Hence their precedence and associativity cannot be changed.
11.1.8 Simultaneous definition of terms and notations
Thanks to reserved notations, the inductive, coinductive, recursive
and corecursive definitions can benefit of customized notations. To do
this, insert a where notation clause after the definition of the
(co)inductive type or (co)recursive term (or after the definition of
each of them in case of mutual definitions). The exact syntax is given
on Figure 11.1. Here are examples:
Coq < Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B
Coq < where "A /\ B" := (and A B).
Coq < Fixpoint plus (n m:nat) {struct n} : nat :=
Coq < match n with
Coq < | O => m
Coq < | S p => S (p+m)
Coq < end
Coq < where "n + m" := (plus n m).
11.1.9 Displaying informations about notations
To deactivate the printing of all notations, use the command
Unset Printing Notations.
To reactivate it, use the command
Set Printing Notations.
The default is to use notations for printing terms wherever possible.
See also: Set Printing All in section 2.8.
11.1.10 Locating notations
To know to which notations a given symbol belongs to, use the command
Locate symbol
where symbol is any (composite) symbol surrounded by quotes. To locate
a particular notation, use a string where the variables of the
notation are replaced by ``_''.
Example:
Coq < Locate "exists".
Notation Scope
"'exists' x : t , p" := ex (fun x : t => p)
: type_scope
(default interpretation)
"'exists' x , p" := ex (fun x => p)
: type_scope
(default interpretation)
Coq < Locate "'exists' _ , _".
Notation Scope
"'exists' x , p" := ex (fun x => p)
: type_scope
(default interpretation)
See also: Section 6.2.10.
| sentence |
::= |
Notation [Local] string := term
[modifiers] [:scope] . |
| |
| |
Infix [Local] string := qualid
[modifiers] [:scope] . |
| |
| |
Reserved Notation [Local] string
[modifiers] . |
| |
| |
Inductive
ind_body [decl_notation] with ... with ind_body [decl_notation]. |
| |
| |
CoInductive
ind_body [decl_notation] with ... with ind_body [decl_notation]. |
| |
| |
Fixpoint
fix_body [decl_notation] with ... with fix_body [decl_notation] . |
| |
| |
CoFixpoint
cofix_body [decl_notation] with ... with cofix_body [decl_notation] . |
| |
| decl_notation |
::= |
[where string := term [:scope]] . |
| |
| modifiers |
::= |
ident , ... , ident at level natural |
| |
| |
ident , ... , ident at next level |
| |
| |
at level natural |
| |
| |
left associativity |
| |
| |
right associativity |
| |
| |
no associativity |
| |
| |
ident ident |
| |
| |
ident global |
| |
| |
ident bigint |
| |
| |
only parsing |
| |
| |
format string |
Figure 11.1: Syntax of the variants of Notation
11.1.11 Notations with recursive patterns
An experimental mechanism is provided for declaring elementary
notations including recursive patterns. The basic syntax is
Coq < Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
On the right-hand-side, an extra construction of the form .. (f
t1 ... tn) .. can be used. Notice that .. is part of
the Coq syntax while ... is just a meta-notation of this
manual to denote a sequence of terms of arbitrary size.
This extra construction enclosed within .., let's call it t,
must be one of the argument of an applicative term of the form (f u1 ... un). The sequences t1 ... tn and
u1 ... un must coincide everywhere but in two places. In
one place, say the terms of indice i, we must have ui = t. In the
other place, say the terms of indice j, both uj and tj must be
variables, say x and y which are bound by the notation string on
the left-hand-side of the declaration. The variables x and y in
the string must occur in a substring of the form "x s .. s
y" where .. is part of the syntax and s is two times the
same sequence of terminal symbols (i.e. symbols which are not
variables).
These invariants must be satisfied in order the notation to be
correct. The term ti is the terminating expression of
the notation and the pattern (f u1 ... ui-1 [I]
ui+1 ... uj-1 [E] uj+1 ... un) is the
iterating pattern. The hole [I] is the iterative place
and the hole [E] is the enumerating place. Remark that if j<i, the
iterative place comes after the enumerating place accordingly.
The notation parses sequences of tokens such that the subpart "x s
.. s y" parses any number of time (but at least one time) a
sequence of expressions separated by the sequence of tokens s. The
parsing phase produces a list of expressions which
are used to fill in order the holes [E] of the iterating pattern
which is nested as many time as the length of the list, the hole [I]
being the nesting point. In the innermost occurrence of the nested
iterating pattern, the hole [I] is finally filled with the terminating
expression.
In the example above, f is cons, n=3 (because cons has
a hidden implicit argument!), i=3 and j=2. The terminating
expression is nil and the iterating pattern is cons
[E] [I]. Finally, the sequence s is made of the single token
``;''. Here is another example.
Coq < Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
Notations with recursive patterns can be reserved like standard
notations, they can also be declared within interpretation scopes (see
section 11.2).
Syntax of notations
The different syntactic variants of the command Notation are
given on Figure 11.1. The optional :scope is
described in the section 11.2.
Remark: No typing of the denoted expression is performed at definition
time. Type-checking is done only at the time of use of the notation.
Remark: Many examples of Notation may be found in the files
composing the initial state of Coq (see directory $COQLIB/theories/Init).
Remark: The notation "{ x }" has a special status in such a way
that complex notations of the form "x + { y }" or
"x * { y }" can be nested with correct precedences. Especially,
every notation involving a pattern of the form "{ x }" is
parsed as a notation where the pattern "{ x }" has been simply
replaced by "x" and the curly brackets are parsed separately.
E.g. "y + { z }" is not parsed as a term of the given form but
as a term of the form "y + z" where z has been parsed
using the rule parsing "{ x }". Especially, level and
precedences for a rule including patterns of the form "{ x }"
are relative not to the textual notation but to the notation where the
curly brackets have been removed (e.g. the level and the associativity
given to some notation, say "{ y } & { z }" in fact applies to
the underlying "{ x }"-free rule which is "y & z").
Persistence of notations
Notations do not survive the end of sections. They survive modules
unless the command Notation Local is used instead of Notation.
11.2 Interpretation scopes
An interpretation scope is a set of notations for terms with
their interpretation. Interpretation scopes provides with a weak,
purely syntactical form of notations overloading: a same notation, for
instance the infix symbol + can be used to denote distinct
definitions of an additive operator. Depending on which interpretation
scopes is currently open, the interpretation is different.
Interpretation scopes can include an interpretation for
numerals. However, this is only made possible at the Objective Caml level.
See Figure 11.1 for the syntax of notations including
the possibility to declare them in a given scope. Here is a typical
example which declares the notation for conjunction in the scope type_scope.
Notation "A /\ B" := (and A B) : type_scope.
Remark: A notation not defined in a scope is called a lonely notation.
11.2.1 Global interpretation rules for notations
At any time, the interpretation of a notation for term is done within
a stack of interpretation scopes and lonely notations. In case a
notation has several interpretations, the actual interpretation is the
one defined by (or in) the more recently declared (or open) lonely
notation (or interpretation scope) which defines this notation.
Typically if a given notation is defined in some scope scope but
has also an interpretation not assigned to a scope, then, if scope
is open before the lonely interpretation is declared, then the lonely
interpretation is used (and this is the case even if the
interpretation of the notation in scope is given after the lonely
interpretation: otherwise said, only the order of lonely
interpretations and opening of scopes matters, and not the declaration
of interpretations within a scope).
The initial state of Coq declares three interpretation scopes and
no lonely notations. These scopes, in opening order, are core_scope, type_scope and nat_scope.
The command to add a scope to the interpretation scope stack is
Open Scope scope.
It is also possible to remove a scope from the interpretation scope
stack by using the command
Close Scope scope.
Notice that this command does not only cancel the last Open Scope
scope but all the invocation of it.
Remark: Open Scope and Close Scope do not survive the end of
sections where they occur. When defined outside of a section, they are
exported to the modules that import the module where they occur.
Variants: - Open Local Scope scope.
- Close Local Scope scope.
These variants are not exported to the modules that import the module
where they occur, even if outside a section.
11.2.2 Local interpretation rules for notations
In addition to the global rules of interpretation of notations, some
ways to change the interpretation of subterms are available.
Local opening of an interpretation scope
It is possible to locally extend the interpretation scope stack using
the syntax (term)%key (or simply term%key
for atomic terms), where key is a special identifier called
delimiting key and bound to a given scope.
In such a situation, the term term, and all its subterms, are
interpreted in the scope stack extended with the scope bound to
key.
To bind a delimiting key to a scope, use the command
Delimit Scope scope with ident
Binding arguments of a constant to an interpretation scope
It is possible to set in advance that some arguments of a given
constant have to be interpreted in a given scope. The command is
Arguments Scope qualid [ opt_scope ... opt_scope ]
where the list is a list made either of _ or of a scope name.
Each scope in the list is bound to the corresponding parameter of
qualid in order. When interpreting a term, if some of the
arguments of qualid are built from a notation, then this notation
is interpreted in the scope stack extended by the scopes bound (if any)
to these arguments.
See also: The command to show the scopes bound to the arguments of a
function is described in section 2.
Binding types of arguments to an interpretation scope
When an interpretation scope is naturally associated to a type
(e.g. the scope of operations on the natural numbers), it may be
convenient to bind it to this type. The effect of this is that any
argument of a function that syntactically expects a parameter of this
type is interpreted using scope. More precisely, it applies only if
this argument is built from a notation, and if so, this notation is
interpreted in the scope stack extended by this particular scope. It
does not apply to the subterms of this notation (unless the
interpretation of the notation itself expects arguments of the same
type that would trigger the same scope).
More generally, any class (see chapter 16) can be
bound to an interpretation scope. The command to do it is
Bind Scope scope with class
Example:
Coq < Parameter U : Set.
U is assumed
Coq < Bind Scope U_scope with U.
Coq < Parameter Uplus : U -> U -> U.
Uplus is assumed
Coq < Parameter P : forall T:Set, T -> U -> Prop.
P is assumed
Coq < Parameter f : forall T:Set, T -> U.
f is assumed
Coq < Infix "+" := Uplus : U_scope.
Coq < Unset Printing Notations.
Coq < Open Scope nat_scope. (* Define + on the nat as the default for + *)
Coq < Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
fun (x y1 y2 : nat) (z : U) (t : nat) =>
P nat (plus x t) (Uplus (f nat (plus y1 y2)) z)
: nat -> nat -> nat -> U -> nat -> Prop
Remark: The scope type_scope has also a local effect on
interpretation. See the next section.
See also: The command to show the scopes bound to the arguments of a
function is described in section 2.
11.2.3 The type_scope interpretation scope
The scope type_scope has a special status. It is a primitive
interpretation scope which is temporarily activated each time a
subterm of an expression is expected to be a type. This includes goals
and statements, types of binders, domain and codomain of implication,
codomain of products, and more generally any type argument of a
declared or defined constant.
11.2.4 Interpretation scopes used in the standard library of Coq
We give an overview of the scopes used in the standard library of
Coq. For a complete list of notations in each scope, use the
commands Print Scopes or Print Scopes scope.
type_scope
This includes infix * for product types and infix + for
sum types. It is delimited by key type.
nat_scope
This includes the standard arithmetical operators and relations on
type nat. Positive numerals in this scope are mapped to their
canonical representent built from O and S. The scope is
delimited by key nat.
N_scope
This includes the standard arithmetical operators and relations on
type N (binary natural numbers). It is delimited by key N
and comes with an interpretation for numerals as closed term of type Z.
Z_scope
This includes the standard arithmetical operators and relations on
type Z (binary integer numbers). It is delimited by key Z
and comes with an interpretation for numerals as closed term of type Z.
positive_scope
This includes the standard arithmetical operators and relations on
type positive (binary strictly positive numbers). It is
delimited by key positive and comes with an interpretation for
numerals as closed term of type positive.
real_scope
This includes the standard arithmetical operators and relations on
type R (axiomatic real numbers). It is delimited by key R
and comes with an interpretation for numerals as term of type R. The interpretation is based on the binary decomposition. The
numeral 2 is represented by 1+1. The interpretation phi(n) of an
odd positive numerals greater n than 3 is 1+(1+1)*phi((n-1)/2).
The interpretation phi(n) of an even positive numerals greater n
than 4 is (1+1)*phi(n/2). Negative numerals are represented as the
opposite of the interpretation of their absolute value. E.g. the
syntactic object -11 is interpreted as -(1+(1+1)*((1+1)*(1+(1+1)))) where the unit 1 and all the operations are
those of R.
bool_scope
This includes notations for the boolean operators. It is
delimited by key bool.
list_scope
This includes notations for the list operators. It is
delimited by key list.
core_scope
This includes the notation for pairs. It is delimited by key core.
11.2.5 Displaying informations about scopes
Print Visibility
This displays the current stack of notations in scopes and lonely
notations that is used to interpret a notation. The top of the stack
is displayed last. Notations in scopes whose interpretation is hidden
by the same notation in a more recently open scope are not
displayed. Hence each notation is displayed only once.
Variant:
Print Visibility scope
This displays the current stack of notations in scopes and lonely
notations assuming that scope is pushed on top of the stack. This
is useful to know how a subterm locally occurring in the scope of
scope is interpreted.
Print Scope scope
This displays all the notations defined in interpretation scope
scope. It also displays the delimiting key if any and the class to
which the scope is bound, if any.
Print Scopes
This displays all the notations, delimiting keys and corresponding
class of all the existing interpretation scopes.
It also displays the lonely notations.
11.3 Abbreviations
An abbreviation is a name denoting a (presumably) more complex
expression. An abbreviation is a special form of notation with no
parameter and only one symbol which is an identifier. This identifier
is given with no quotes around. Example:
Coq < Notation List := (list nat).
An abbreviation expects no precedence nor associativity, since it can
always be put at the lower level of atomic expressions, and
associativity is irrelevant. Abbreviations are used as much as
possible by the Coq printers unless the modifier
(only parsing) is given.
Abbreviations are bound to an absolute name like for an ordinary
definition, and can be referred by partially qualified names too.
Abbreviations are syntactic in the sense that they are bound to
expressions which are not typed at the time of the definition of the
abbreviation but at the time it is used. Especially, abbreviation can
be bound to terms with holes (i.e. with ``_''). The general syntax
for abbreviations is
Notation [Local] ident := term
[(only parsing)] .
Example:
Coq < Definition explicit_id (A:Set) (a:A) := a.
explicit_id is defined
Coq < Notation id := (explicit_id _).
Coq < Check (id 0).
id 0
: nat
Abbreviations do not survive the end of sections. No typing of the denoted
expression is performed at definition time. Type-checking is done only
at the time of use of the abbreviation.
Remark: compatibility Abbreviations are similar to the syntactic
definitions available in versions of Coq prior to version 8.0,
except that abbreviations are used for printing (unless the modifier
(only parsing) is given) while syntactic definitions were not.
11.4 Tactic Notations
Tactic notations allow to customize the syntax of the tactics of the
tactic language3. Tactic notations obey the following
syntax
| sentence |
::= |
Tactic Notation string [production_item ... production_item] |
| |
|
:= tactic . |
| production_item |
::= |
string | tactic_argument_type(ident) |
| tactic_argument_type |
::= |
ident |
simple_intropattern |
hyp |
| |
| |
reference |
constr |
| |
| |
integer |
| |
| |
int_or_var |
tactic | |
A tactic notation Tactic Notation string [production_item ... production_item]
:= tactic extends the parser and pretty-printer of tactics with a
new rule made of the juxtaposition of the head name of the tactic
string and the list of its production items (in the syntax of
production items, string stands for a terminal symbol and tactic_argument_type(ident) for non terminal entries. It then evaluates
into the tactic expression tactic.
Each type of tactic argument has a specific semantic regarding how it
is parsed and how it is interpreted. The semantic is described in the
following table. The last command gives examples of tactics which
use the corresponding kind of argument.
| Tactic argument type |
parsed as |
interpreted as |
as in tactic |
| |
| ident |
identifier |
a user-given name |
intro |
| simple_intropattern |
intro_pattern |
an intro_pattern |
intros |
| hyp |
identifier |
an hypothesis defined in context |
clear |
| reference |
qualified identifier |
a global reference of term |
unfold |
| constr |
term |
a term |
exact |
| integer |
integer |
an integer |
|
| int_or_var |
identifier or integer |
an integer |
do |
| tactic |
tactic |
a tactic |
|
Remark: In order to be bound in tactic definitions, each syntactic entry
for argument type must include the case of simple Ltac identifier
as part of what it parses. This is naturally the case for ident,
simple_intropattern, reference, constr, ... but not
for integer. This is the reason for introducing a special entry
int_or_var which evaluates to integers only but which
syntactically includes identifiers in order to be usable in tactic
definitions.
- 1
- which are the levels effectively chosen in the
current implementation of Coq
- 2
-
Coq accepts notations declared as no associative but the parser on
which Coq is built, namely Camlp4, currently does not implement the
no-associativity and replace it by a left associativity; hence it is
the same for Coq: no-associativity is in fact left associativity
- 3
- Tactic notations are just a simplification of
the Grammar tactic simple_tactic command that existed in
versions prior to version 8.0.