[isabelle] Commandline results for quickcheck / nitpick
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Commandline results for quickcheck / nitpick
- From: Alex Weisberger <alex.m.weisberger at gmail.com>
- Date: Sun, 14 Nov 2021 00:05:30 -0500
- Authentication-results: cam.ac.uk; iprev=pass (mail-lf1-f42.google.com) smtp.remote-ip=184.108.40.206; spf=pass smtp.mailfrom=gmail.com; dkim=pass header.d=gmail.com header.s=20210112 header.a=rsa-sha256; arc=none
quickcheck and nitpick provide great feedback within the jedit IDE. Using "isabelle build" to build a theory containing one of these commands doesn't work, however. It's possible that I'm doing something wrong, but it seems like a theory is invalid if it contains one of these commands. Is this true - are they only for interaction purposes, not to count as results of the theory?
This would make sense, since the goal is a checked proof after all. Still, it is convenient to see these counterexamples sometimes, and seeing them from the command line would be nice.
Does anyone have any useful information regarding this? Thanks.
This archive was generated by a fusion of
Pipermail (Mailman edition) and