*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 02 Jul 2015 08:21:45 +0200*In-reply-to*: <5594D6B7.1080109@in.tum.de>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com> <5594D6B7.1080109@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Should it not at least show the interpretation of the free type variable? Manuel On 02/07/15 08:14, Tobias Nipkow wrote: > > 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 > > No type constraints. Because 3, 4 and < are polymorphic, quickcheck is > free to build a type/model with an interpretation for < where 3 < 4 > does not hold. > > There used to be a time when the interface alerted you to polymorphic > numerals, which are almost always not what one wants. But we have > moved on from that. > > The fact that you are not shown the model is because only the > interpretation of the free variables is shown, but there are none. > > 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 >> >

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

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

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

- Previous by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Previous by Thread: Re: [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