[isabelle] Quickcheck counter example of "3 < 4"?



I forgot to add a type annotation and ended up with the following (Isabelle
2015 on Windows 7):

lemma "3 < 4" quickcheck
Quickchecking...
For instantiation with default_type Enum.finite_1:
Enum.finite_1 to be substituted for variable 'a does not have sort
{numeral,ord}
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found no counterexample.

Note: in the first case it says there is a counter example but that is the
end of the output in the "Output" tab of jEdit.

Is this to be expected when no types are given? As a new Isabelle user it
quite surprised me.

Thanks,
Jason



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.