[isabelle] Quickcheck ML



Hi,

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?

Best,
Moa




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