# HG changeset patch
# User blanchet
# Date 1280835624 -7200
# Node ID ef644a533265e8530b100f7449af771ac0a5210e
# Parent  c15dfe7bc077ead7ecc8046846eb7d592c90b4bb
choose better example

diff -r c15dfe7bc077 -r ef644a533265 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Aug 03 13:29:26 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Aug 03 13:40:24 2010 +0200
@@ -2649,30 +2649,30 @@
 definition as follows:
 
 \prew
-\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_alt_def}$ [\textit{nitpick\_def}]:\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
 = 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)$''
+\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})$''
+\textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]: \\
+``$\textit{odd~x} = \lnot\, \textit{even}~x$''
 \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\/}$''
+\textbf{lemma} \textit{odd\_psimps} [\textit{nitpick\_simp}]: \\
+``$\textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{False\/}$'' \\
+``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
 \postw
 
 Such tweaks should be done with great care, because Nitpick will assume that the