Email Gateway (Aug 18 2022 at 18:59): Email Gateway (Aug 18 2022 at 18:59):From: Omar Montano Rivas <O.Montano-Rivas-2@sms.ed.ac.uk>
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."
Last updated: Apr 23 2024 at 08:19 UTC