[isabelle] Signatures for counter-example checkers



Hi,

I am interested in the values of free variables that refute a conjecture. For this, I am using Quickcheck's function 'quickcheck : (string * string list) list -> int -> Proof.state -> (string * term) list option' from the ML level. I was wondering whether it is possible to obtain this information from Refute and Nitpick. Checking at Refute's signature, it seems to have the function 'refute_term : Proof.context -> (string * string) list -> term list -> term -> unit' which I have copied/rewrited to obtain 'my_refute_term : Proof.context -> (string * string) list -> term list -> term -> (term * term) list option' and gain this functionality. Can something like that be added to Refute/Nitpick signatures?

BTW, excellent tools!

Best,

Omar.

"The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336."

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.







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