294 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] |
294 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] |
295 \hbox{}\qquad Free variables: \nopagebreak \\ |
295 \hbox{}\qquad Free variables: \nopagebreak \\ |
296 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ |
296 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ |
297 \hbox{}\qquad\qquad $x = a_3$ \\ |
297 \hbox{}\qquad\qquad $x = a_3$ \\ |
298 \hbox{}\qquad Constant: \nopagebreak \\ |
298 \hbox{}\qquad Constant: \nopagebreak \\ |
299 \hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$ |
|
300 \postw |
|
301 |
|
302 We can see more clearly now. Since the predicate $P$ isn't true for a unique |
|
303 value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even |
|
304 $a_1$. Since $P~a_1$ is false, the entire formula is falsified. |
|
305 |
|
306 As an optimization, Nitpick's preprocessor introduced the special constant |
|
307 ``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e., |
|
308 $\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$ |
|
309 satisfying $P~y$. We disable this optimization by passing the |
|
310 \textit{full\_descrs} option: |
|
311 |
|
312 \prew |
|
313 \textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount] |
|
314 \slshape |
|
315 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] |
|
316 \hbox{}\qquad Free variables: \nopagebreak \\ |
|
317 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ |
|
318 \hbox{}\qquad\qquad $x = a_3$ \\ |
|
319 \hbox{}\qquad Constant: \nopagebreak \\ |
|
320 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ |
299 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ |
321 \postw |
300 \postw |
322 |
301 |
323 As the result of another optimization, Nitpick directly assigned a value to the |
302 As the result of an optimization, Nitpick directly assigned a value to the |
324 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we |
303 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we |
325 disable this second optimization by using the command |
304 disable this optimization by using the command |
326 |
305 |
327 \prew |
306 \prew |
328 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\, |
307 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}] |
329 \textit{show\_consts}] |
308 \postw |
330 \postw |
309 |
331 |
310 we get \textit{The}: |
332 we finally get \textit{The}: |
|
333 |
311 |
334 \prew |
312 \prew |
335 \slshape Constant: \nopagebreak \\ |
313 \slshape Constant: \nopagebreak \\ |
336 \hbox{}\qquad $\mathit{The} = \undef{} |
314 \hbox{}\qquad $\mathit{The} = \undef{} |
337 (\!\begin{aligned}[t]% |
315 (\!\begin{aligned}[t]% |
2488 domain, but it is usually more efficient. |
2466 domain, but it is usually more efficient. |
2489 |
2467 |
2490 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug} |
2468 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug} |
2491 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).} |
2469 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).} |
2492 |
2470 |
2493 \optrue{fast\_descrs}{full\_descrs} |
|
2494 Specifies whether Nitpick should optimize the definite and indefinite |
|
2495 description operators (THE and SOME). The optimized versions usually help |
|
2496 Nitpick generate more counterexamples or at least find them faster, but only the |
|
2497 unoptimized versions are complete when all types occurring in the formula are |
|
2498 finite. |
|
2499 |
|
2500 {\small See also \textit{debug} (\S\ref{output-format}).} |
2471 {\small See also \textit{debug} (\S\ref{output-format}).} |
2501 |
2472 |
2502 \opnodefault{whack}{term\_list} |
2473 \opnodefault{whack}{term\_list} |
2503 Specifies a list of atomic terms (usually constants, but also free and schematic |
2474 Specifies a list of atomic terms (usually constants, but also free and schematic |
2504 variables) that should be taken as being $\unk$ (unknown). This can be useful to |
2475 variables) that should be taken as being $\unk$ (unknown). This can be useful to |