# HG changeset patch
# User blanchet
# Date 1280838524 -7200
# Node ID 0cea0125339a442b38a5a0c3a5c884e31434202a
# Parent  84c3d801bddadda2d4693071144298d379703c22
more documentation, based on email discussions with a user

diff -r 84c3d801bdda -r 0cea0125339a doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Aug 03 14:06:29 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Aug 03 14:28:44 2010 +0200
@@ -2648,7 +2648,7 @@
 \postw
 
 By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
-the introduction rules. To override this, we can specify an alternative
+the introduction rules. To override this, you can specify an alternative
 definition as follows:
 
 \prew
@@ -2656,7 +2656,7 @@
 \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:
+= 1$. Alternatively, you 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)$''
@@ -2690,11 +2690,23 @@
 \prew
 \textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\
 ``$\textit{optimum}~t =
-     (\forall u.\; \textit{consistent~u} \mathrel{\land} \textit{alphabet~t} = \textit{alphabet~u}$ \\
+     (\forall u.\; \textit{consistent}~u \mathrel{\land} \textit{alphabet}~t = \textit{alphabet}~u$ \\
 \phantom{``$\textit{optimum}~t = (\forall u.\;$}${\mathrel{\land}}\; \textit{freq}~t = \textit{freq}~u \longrightarrow
-         \textit{cost~t} \le \textit{cost~u})$''
+         \textit{cost}~t \le \textit{cost}~u)$''
 \postw
 
+In some rare occasions, you might want to provide an inductive or coinductive
+view on top of an existing constant $c$. The easiest way to achieve this is to
+define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$
+and let Nitpick know about it:
+
+\prew
+\textbf{lemma} \textit{c\_alt\_def} [\textit{nitpick\_def}]:\kern.4em ``$c \equiv c'$\kern2pt ''
+\postw
+
+This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive
+definition.
+
 \section{Standard ML Interface}
 \label{standard-ml-interface}