--- a/doc-src/Nitpick/nitpick.tex Tue Aug 03 12:31:30 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Tue Aug 03 13:17:15 2010 +0200
@@ -2602,7 +2602,6 @@
\nopagebreak
This attribute specifies the (free-form) specification of a constant defined
using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
-
\end{enum}
When faced with a constant, Nitpick proceeds as follows:
@@ -2660,6 +2659,22 @@
\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
\postw
+Moreover, because of its internal three-valued logic, Nitpick tends to lose a
+lot of precision in the presence of partially specified constants. For example,
+
+\prew
+\textbf{lemma} $\mathit{list\_of\_LCons}$ [\textit{nitpick\_simp}]: \\
+``$\textit{list\_of}~(\textit{LCons~x~xs}) = {}$ \\
+\phantom{``}$(\textrm{if}~\textit{lfinite~xs}~\textrm{then}~x \mathbin{\#} \textit{list\_of~xs}~\textrm{else}~\textit{undefined})$''
+\postw
+
+is superior to
+
+\prew
+\textbf{lemma} $\mathit{list\_of\_LCons}$ [\textit{nitpick\_psimp}]: \\
+``$\textit{lfinite~xs} \,\Longrightarrow\, \textit{list\_of}~(\textit{LCons~x~xs}) = x \mathbin{\#} \textit{list\_of~xs\/}$''
+\postw
+
Such tweaks should be done with great care, because Nitpick will assume that the
constant is completely defined by its equational specification. For example, if
you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define