[isabelle] quickcheck and error constants



Hello,

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?

Thanks,
-john







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