Re: [isabelle] quickcheck and error constants
Here's a solution (with only one int argument - trust you can generalize ;-)
consts cerror :: "int => string => 'a"
"cerror" ("(fn i => (fn x => error(implode x)))")
definition f where "f i == if i < 0 then cerror i ''x'' else i"
lemma "f x = x"
The implode is required because HOL's strings are implemented as char lists.
However, there are two things that puzzle me, that the implementor might
be able to comment on:
1. autoquickcheck does seem to kick in or its result is hidden...
2. If in the ML code for cerror I replace the i by _, I have a problem:
the generatd ML does not type check...
John Matthews schrieb:
I am trying to provide a shallow embedding of the Cryptol primitive
"cerror :: int => int => string => 'a". Logically this is an undefined
value, but I'd like Isabelle's quickcheck command to compile the Cryptol
expression "cerror a b str" into the SML expression "error str", so that
quickcheck throws an exception if cerror s ever executed during a run.
How do I define cerror appropriately?
This archive was generated by a fusion of
Pipermail (Mailman edition) and