*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 02 Jul 2015 08:14:15 +0200*In-reply-to*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

On 02/07/2015 07:48, Jason Dagit wrote:

I forgot to add a type annotation and ended up with the following (Isabelle 2015 on Windows 7): lemma "3 < 4" quickcheck

Tobias

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Manuel Eberl

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Jason Dagit

**References**:**[isabelle] Quickcheck counter example of "3 < 4"?***From:*Jason Dagit

- Previous by Date: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Previous by Thread: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list