\savebox{\tmpxyz}[0.9\linewidth]{
\begin{minipage}{0.9\linewidth}
\ensuremath{#1} \\
- --------------------------\\ % come si fa una linea orizzontale?
+ \rule{3cm}{0.03cm}\\
\ensuremath{#2}
\end{minipage}}\setlength{\fboxsep}{3mm}%
\begin{center}
Matita benefits of a graphical interface and a powerful MathML rendering
widget that allows the user to select pieces of the sequent he is working
on. While this is an extremely intuitive way for the user to
-restrict the application of a tactic, for example, to some subterms of the
+restrict the application of tactics, for example, to some subterms of the
conclusion or some hypothesis, the way this action is recorded to the text
script is not obvious.\\
In \MATITA{} this issue is addressed by patterns.
\subsubsection{Pattern syntax}
A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
$\NT{wanted}$.
-The former mocks-up a sequent, replacing unwanted subterms with $?$ and
+The former mocks-up a sequent, discharging unwanted subterms with $?$ and
selecting the interesting parts with the placeholder $\%$.
The latter is a term that lives in the context of the placeholders.
$\NT{sequent\_path}$, while the second
one searches the $\NT{wanted}$ term starting from these roots. Both are
optional steps, and by convention the empty pattern selects the whole
-goal.
+conclusion.
\begin{description}
\item[Phase 1]
\end{grafite}
\noindent
This pattern, that is a simple instance of the $\NT{sequent\_path}$
-grammar entry, acts on $H$ that has type (without notation)
-$(eq~nat~(m+n)~n)$ and discharges the head of the application and the
-first two arguments with a $?$ and selects the last argument with
-$\%$. The syntax may seem uncomfortable, but the user can simply
-select with the mouse the right part of the equivalence and left to the
-system the burden of writing down in the script file the corresponding
-pattern with $?$ and $\%$ in the right place (expecially where implicit
-arguments are hidden by the notation, like the type $nat$ in this
-example).
+grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
+and discharges the head of the application and the first two arguments with a
+$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
+but the user can simply select with the mouse the right part of the equivalence
+and left to the system the burden of writing down in the script file the
+corresponding pattern with $?$ and $\%$ in the right place (that is not
+trivial, expecially where implicit arguments are hidden by the notation, like
+the type $nat$ in this example).
Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
works too and can be done, by the experienced user, writing directly
\noindent
\subsubsection{Tactics supporting patterns}
-In \MATITA{} the following tactics can be restricted to subterms of
-the working sequent: simplify, change, fold, unfold, generalize, replace and
-rewrite.
+In \MATITA{} all the tactics that can be restricted to subterm of the working
+sequent accept the pattern syntax. In particular these tactics are: simplify,
+change, fold, unfold, generalize, replace and rewrite.
+
\NOTE{attualmente rewrite e \\ fold non supportano \\ phase 2. per
supportarlo\\bisogna far loro trasformare\\il pattern phase1+phase2\\
in un pattern phase1only\\come faccio nell'ultimo esempio.\\lo si fa
to change only the left part of the equivalence, the correct command
is
\begin{grafite}
- change n at 2 in H with (O + H)
+ change n at 2 in H with (O + n)
\end{grafite}
\noindent
meaning that in the hypothesis $H$ the $n$ we want to change is the
unification.
The idea behind this way of identifying subterms in not really far
-from the idea behind patterns patterns, but really fails in help using
-complex notation, since it relays on the way the user sees the
-sequent. Notation can swap arguments, or place them upside-down or
-even put them inside a bidimensional matrix. In these cases using the
-mouse to select the wanted term is probably the only way to tell the
-system exactly what you want to do.
+from the idea behind patterns, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.
+In these cases using the mouse to select the wanted term is probably the
+only way to tell the system exactly what you want to do.
One of the goals of \MATITA{} is to use modern publishing techiques, and
adopting a method for restricting tactics application domain that discourages
\subsection{tatticali}
\ASSIGNEDTO{gares}
+\begin{verbatim}
+
+\end{verbatim}
+
\subsection{Disambiguation}
\label{sec:disambiguation}
\ASSIGNEDTO{zack}
projects / helm.git / blobdiff