equal
deleted
inserted
replaced
738 |
738 |
739 Let's try an example: |
739 Let's try an example: |
740 |
740 |
741 \prew |
741 \prew |
742 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ |
742 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ |
743 \textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount] |
743 \textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] |
744 \slshape The inductive predicate ``\textit{even}'' was proved well-founded. |
744 \slshape The inductive predicate ``\textit{even}'' was proved well-founded. |
745 Nitpick can compute it efficiently. \\[2\smallskipamount] |
745 Nitpick can compute it efficiently. \\[2\smallskipamount] |
746 Trying 1 scope: \\ |
746 Trying 1 scope: \\ |
747 \hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount] |
747 \hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount] |
748 Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount] |
748 Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount] |
756 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the |
756 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the |
757 existential quantifier: |
757 existential quantifier: |
758 |
758 |
759 \prew |
759 \prew |
760 \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ |
760 \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ |
761 \textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount] |
761 \textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount] |
762 \slshape Nitpick found a counterexample: \\[2\smallskipamount] |
762 \slshape Nitpick found a counterexample: \\[2\smallskipamount] |
763 \hbox{}\qquad Empty assignment |
763 \hbox{}\qquad Empty assignment |
764 \postw |
764 \postw |
765 |
765 |
766 So far we were blessed by the wellfoundedness of \textit{even}. What happens if |
766 So far we were blessed by the wellfoundedness of \textit{even}. What happens if |
1750 formula at hand, preferring the binary notation for problems involving |
1750 formula at hand, preferring the binary notation for problems involving |
1751 multiplicative operators or large constants. |
1751 multiplicative operators or large constants. |
1752 |
1752 |
1753 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for |
1753 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for |
1754 problems that refer to the types \textit{rat} or \textit{real} or the constants |
1754 problems that refer to the types \textit{rat} or \textit{real} or the constants |
1755 \textit{gcd} or \textit{lcm}. |
1755 \textit{Suc}, \textit{gcd}, or \textit{lcm}. |
1756 |
1756 |
1757 {\small See also \textit{bits} (\S\ref{scope-of-search}) and |
1757 {\small See also \textit{bits} (\S\ref{scope-of-search}) and |
1758 \textit{show\_datatypes} (\S\ref{output-format}).} |
1758 \textit{show\_datatypes} (\S\ref{output-format}).} |
1759 |
1759 |
1760 \opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$} |
1760 \opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$} |