Re: [isabelle] emergence of "TERM _" (using quickcheck and nitpick)



Dear Daniel,

Am 20.11.2014 um 19:21 schrieb Daniel Raggi <danielraggi at gmail.com>:

> I'm getting exceptions and having other kinds of problems when using
> quickcheck or nitpick inside tactics
[...]
> .Nitpicking goal:
>  TERM _.
> 
> and finds nothing.
> 
> Does anyone know what this is about?

From this output, it would appear that the issue has nothing to do with Quickcheck and Nitpick, and everything to do with the string of tactics that were applied before you called those tools and that gave rise to "TERM _" (which I also don't know, but it looks like some dummy placeholder produced by some odd tactic).

Regards,

Jasmin





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