# HG changeset patch # User blanchet # Date 1291719416 -3600 # Node ID 8e2f2398aae719885f0c4b4355b032b086ec93c1 # Parent 3db267a01c1d59adfdf406a304955fb338ef04e7 updated Nitpick's documentation w.r.t. finitization diff -r 3db267a01c1d -r 8e2f2398aae7 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Dec 07 11:56:53 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Tue Dec 07 11:56:56 2010 +0100 @@ -2108,14 +2108,9 @@ per-type basis using the \textit{box}~\qty{type} option described above. \opargboolorsmart{finitize}{type}{dont\_finitize} -Specifies whether Nitpick should attempt to finitize a given type, which can be -a function type or an infinite ``shallow datatype'' (an infinite datatype whose -constructors don't appear in the problem). - -For function types, Nitpick performs a monotonicity analysis to detect functions -that are constant at all but finitely many points (e.g., finite sets) and treats -such occurrences specially, thereby increasing the precision. The option can -then take the following values: +Specifies whether Nitpick should attempt to finitize an infinite ``shallow +datatype'' (an infinite datatype whose constructors don't appear in the +problem). The option can then take the following values: \begin{enum} \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type. @@ -2132,12 +2127,9 @@ genuine.'' \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype. \item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to -detect whether the datatype can be safely finitized before finitizing it. +detect whether the datatype can be soundly finitized before finitizing it. \end{enum} -Like other drastic optimizations, finitization can sometimes prevent the -discovery of counterexamples. - \nopagebreak {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono} (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and