doc-src/Nitpick/nitpick.tex

 \flushitem{\textit{nitpick\_choice\_spec}}
 
 \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:
 
 \begin{enum}

 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
 = 1$. Alternatively, we can specify an equational specification of the constant:
 
 \prew
 \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