Re: [isabelle] Quickcheck problem?

Hi Thomas,

> I am playing a bit with Isabelle (MacOSX version, Isabelle2009-2.dmg)
> and had the following problem: quickcheck always answers
> *** Term to be tested contains type variables
> *** At command "quickcheck".
> whatever the theorem to be proved.

> theory ToyList3
> imports Datatype
> begin

The issue is actually located here: in user space, you are always
expected to include the Main theory among you imports (directly or
transitively).  The toy list examples in the tutorial are just there to
demonstrate for beginners how lists are done in the system, therefore
they start at a theory which does not contain lists already.

Beneath theory Main there is an intricate bootstrap of various
components which are then plugged together to get the basic tool setup
that the user expects:  also quickcheck is not monolithic but can be
thought of as a "microkernel service".  The good thing is that as a user
you need not spend much thought on it: start with Main and leave the
issues beneath to developers.  An analogy: starting beneath Main is like
using a Unix without init or Upstart.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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