Re: [isabelle] quickcheck and error constants

Tobias Nipkow wrote:
> However, there are two things that puzzle me, that the implementor might
> be able to comment on:
> 1. autoquickcheck does seem to kick in or its result is hidden...

auto quickcheck only outputs something if it finds a counterexample,
i.e. the goal evaluates to False. If the code generator signals an error
because the current goal is not executable, the compilation of the generated
code fails because it is ill-formed, or an exception is raised during the
execution of the code, this is silently ignored. The rationale behind this
was to prevent auto quickcheck from displaying too many "spam messages" that
might confuse users.

> 2. If in the ML code for cerror I replace the i by _, I have a problem:
> the generatd ML does not type check...

The problem is that _ has a special meaning: like in mixfix templates,
the _ in a declaration

    f ("...")

indicates a position in the ML code "..." where code for the arguments of f
should be inserted (see e.g. the definition of "+" in the Int theory). If
you want a _ to occur in the ML code, you have to escape it by writing '_
(like in mixfix templates).


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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