[isabelle] Quickcheck ML
I'm currently updating IsaPlanner and IsaCoSy to Isabelle2012. Both systems make use of Isabelle's counterexample checker quickcheck, which has been updated. I need to send lists of things of type term for testing, so I'm assuming I need to use the test_term function, which has type
Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
I'd like to know what the last argument of type (term * term list) list is representing? Which list is the list of terms I want to counter-example check, and what does the first term in the pair represent?
This archive was generated by a fusion of
Pipermail (Mailman edition) and