src/Doc/Nitpick/document/root.tex

 \label{coinductive-datatypes}
 
 A coinductive datatype is similar to an inductive datatype but
 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
-1, 2, 3, \ldots]$ can be defined as lazy lists using the
+1, 2, 3, \ldots]$ can be defined as coinductive lists, or ``lazy lists,'' using the
 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
 
 Although it is otherwise no friend of infinity, Nitpick can find counterexamples

 \label{standard-ml-interface}
 
 Nitpick provides a rich Standard ML interface used mainly for internal purposes
 and debugging. Among the most interesting functions exported by Nitpick are
 those that let you invoke the tool programmatically and those that let you
-register and unregister custom coinductive datatypes as well as term
-postprocessors.
-
-\subsection{Invocation of Nitpick}
-\label{invocation-of-nitpick}
+register and unregister custom term postprocessors as well as coinductive
+datatypes.
+
+\subsection{Invoking Nitpick}
+\label{invoking-nitpick}
 
 The \textit{Nitpick} structure offers the following functions for invoking your
 favorite counterexample generator:
 
 \prew

 $\hbox{}\quad\textit{Nitpick.pick\_nits\_in\_subgoal}~\textit{state}~\textit{params}~\textit{Nitpick.Normal}~\textit{i}~\textit{n}$
 \postw
 
 \let\antiq=\textrm
 
-\subsection{Registration of Coinductive Datatypes}
-\label{registration-of-coinductive-datatypes}
-
-If you have defined a custom coinductive datatype, you can tell Nitpick about
-it, so that it can use an efficient Kodkod axiomatization similar to the one it
-uses for lazy lists. The interface for registering and unregistering coinductive
-datatypes consists of the following pair of functions defined in the
-\textit{Nitpick\_HOL} structure:
-
-\prew
-$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
-$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
-$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
-$\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
-$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
-\postw
-
-The type $'a~\textit{llist}$ of lazy lists is already registered; had it
-not been, you could have told Nitpick about it by adding the following line
-to your theory file:
-
-\prew
-$\textbf{declaration}~\,\{{*}$ \\
-$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
-$\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
-$\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
-${*}\}$
-\postw
-
-The \textit{register\_codatatype} function takes a coinductive datatype, its
-case function, and the list of its constructors (in addition to the current
-morphism and generic proof context). The case function must take its arguments
-in the order that the constructors are listed. If no case function with the
-correct signature is available, simply pass the empty string.
-
-On the other hand, if your goal is to cripple Nitpick, add the following line to
-your theory file and try to check a few conjectures about lazy lists:
-
-\prew
-$\textbf{declaration}~\,\{{*}$ \\
-$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
-${*}\}$
-\postw
-
-Inductive datatypes can be registered as coinductive datatypes, given
-appropriate coinductive constructors. However, doing so precludes
-the use of the inductive constructors---Nitpick will generate an error if they
-are needed.
-
-\subsection{Registration of Term Postprocessors}
-\label{registration-of-term-postprocessors}
+\subsection{Registering Term Postprocessors}
+\label{registering-term-postprocessors}
 
 It is possible to change the output of any term that Nitpick considers a
 datatype by registering a term postprocessor. The interface for registering and
 unregistering postprocessors consists of the following pair of functions defined
 in the \textit{Nitpick\_Model} structure:

 $\hbox{}\quad\textit{typ} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic}$
 \postw
 
 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
 \texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
+
+\subsection{Registering Coinductive Datatypes}
+\label{registering-coinductive-datatypes}
+
+If you have defined a custom coinductive datatype, you can tell Nitpick about
+it, so that it can use an efficient Kodkod axiomatization similar to the one it
+uses for lazy lists. The interface for registering and unregistering coinductive
+datatypes consists of the following pair of functions defined in the
+\textit{Nitpick\_HOL} structure:
+
+\prew
+$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
+$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
+$\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
+\postw
+
+The type $'a~\textit{llist}$ of lazy lists is already registered; had it
+not been, you could have told Nitpick about it by adding the following line
+to your theory file:
+
+\prew
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
+$\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
+${*}\}$
+\postw
+
+The \textit{register\_codatatype} function takes a coinductive datatype, its
+case function, and the list of its constructors (in addition to the current
+morphism and generic proof context). The case function must take its arguments
+in the order that the constructors are listed. If no case function with the
+correct signature is available, simply pass the empty string.
+
+On the other hand, if your goal is to cripple Nitpick, add the following line to
+your theory file and try to check a few conjectures about lazy lists:
+
+\prew
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+${*}\}$
+\postw
+
+Inductive datatypes can be registered as coinductive datatypes, given
+appropriate coinductive constructors. However, doing so precludes
+the use of the inductive constructors---Nitpick will generate an error if they
+are needed.
 
 \section{Known Bugs and Limitations}
 \label{known-bugs-and-limitations}
 
 Here are the known bugs and limitations in Nitpick at the time of writing: