- concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
- part of the syntax. $\NT{ident}$ is an hypothesis name and
- selects the assumption where the following optional $\NT{multipath}$
- will operate. \verb+\vdash+ can be considered the name for the goal.
- If the whole pattern is omitted, the whole goal will be selected.
- If one or more hypotheses names are given the selection is restricted to
- these assumptions. If a $\NT{multipath}$ is omitted the whole
- assumption is selected. Remember that the user can be mostly
- unaware of this syntax, since the system is able to write down a
- $\NT{sequent\_path}$ starting from a visual selection.
- \NOTE{Questo ancora non va in matita}
-
- A $\NT{multipath}$ is a CIC term in which a special constant $\%$
- is allowed.
- The roots of discharged subterms are marked with $?$, while $\%$
- is used to select roots. The default $\NT{multipath}$, the one that
- selects the whole term, is simply $\%$.
- Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
- that respectively select the first argument of an application or
- the source of an arrow and the head of the application that is
- found in the arrow target.
-
- The first phase not only selects terms (roots of subterms) but
- determines also their context that will be eventually used in the
- second phase.
+ concerns only \NT{sequent\_path}. \NT{ident} is an hypothesis name and selects
+ the assumption where the following optional \NT{multipath} will operate.
+ \verb+\vdash+ can be considered the name for the goal. If the whole pattern
+ is omitted, the whole goal will be selected. If one or more hypothesis names
+ are given, the selection is restricted to that assumptions. If a
+ $\NT{multipath}$ is omitted the whole assumption is selected. Remember that
+ the user can be mostly unaware of patterns concrete syntax, since the system
+ is able to write down a \NT{sequent\_path} starting from a graphical
+ selection.\NOTE{Questo ancora non va in matita}
+
+ A \NT{multipath} is a CIC term in which a special constant \OP{\%} is allowed.
+ The roots of discharged subterms are marked with \OP{?}, while \OP{\%} is used
+ to select roots. The default \NT{multipath}, the one that selects the whole
+ term, is simply \OP{\%}. Valid \NT{multipath} are, for example, \texttt{(? \%
+ ?)} or \texttt{\% \TEXMACRO{to} (\% ?)} that respectively select the first
+ argument of an application or the source of an arrow and the head of the
+ application that is found in the arrow target.
+
+ This phase not only selects terms (roots of subterms) but determines also
+ their context that will be possibly used in the next phase.