author blanchet Mon, 21 Feb 2011 11:50:38 +0100 changeset 41796 afd7405f1d7e parent 41795 79a79460b70c child 41797 0c6093d596d6
updated docs w.r.t. "nitpick_unfold" attribute
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:38 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:38 2011 +0100
@@ -2536,12 +2536,12 @@
following attributes to affect Nitpick's behavior:

\begin{enum}
-\flushitem{\textit{nitpick\_def}}
+\flushitem{\textit{nitpick\_unfold}}

\nopagebreak
-This attribute specifies an alternative definition of a constant. The
-alternative definition should be logically equivalent to the constant's actual
-axiomatic definition and should be of the form
+This attribute specifies an equation that Nitpick should use to expand a
+constant. The equation should be logically equivalent to the constant's actual
+definition and should be of the form

\qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$,

@@ -2550,7 +2550,8 @@
\qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,

where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
-$t$.
+$t$. Each occurrence of $c$ in the problem is expanded to $\lambda x_1\,\ldots +x_n.\; t$.

\flushitem{\textit{nitpick\_simp}}

@@ -2603,8 +2604,8 @@
uses these theorems as the specification of the constant.

\item[4.] Otherwise, it looks up the definition of the constant. If the
-\textit{nitpick\_def} set associated with the constant is not empty, it uses the
-latest rule added to the set as the definition of the constant; otherwise it
+\textit{nitpick\_unfold} set associated with the constant is not empty, it uses
+the latest rule added to the set as the definition of the constant; otherwise it
uses the actual definition axiom.

\begin{enum}
@@ -2641,7 +2642,7 @@
definition as follows:

\prew
-\textbf{lemma} $\mathit{odd\_alt\_def}$ [\textit{nitpick\_def}]:\kern.4em $\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_alt\_unfold}$ [\textit{nitpick\_unfold}]:\kern.4em $\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
\postw

Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2 @@ -2691,7 +2692,7 @@ and let Nitpick know about it: \prew -\textbf{lemma} \textit{c\_alt\_def} [\textit{nitpick\_def}]:\kern.4em $c \equiv c'$\kern2pt '' +\textbf{lemma} \textit{c\_alt\_unfold} [\textit{nitpick\_unfold}]:\kern.4em $c \equiv c'$\kern2pt '' \postw This ensures that Nitpick will substitute$c'$for$c\$ and use the (co)inductive