Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error



On 1/17/2013 2:12 PM, Gottfried Barrow wrote:
function sFOLf :: "sFOLdt => bool" where

Please change "function" to "fun".

It still works out the same. Without the "Forall" lines in my "datatype" and "fun", my sFOLf function terminates correctly with the message "Found termination order: "{}"".

Thanks,
GB






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