Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
On 1/17/2013 11:35 PM, John Wickerson wrote:
The problem is here...
function sFOLf :: "sFOLdt => bool" where
"sFOLf (Forall u f) = (!u. f)"
That said, I haven't tested this in Isabelle, so I might be way off the mark.
No, you're on the mark. Thanks for the tip. That gets rid of that
particular error, but there are some major problems still. I'm not doing
any real recursion. Like for this statement,
"sFOLf (And f1 f2) = (f1 & f2)",
I would need to recurse on f1 and f2, but I'm not even close; that's all
messed up. I get an error from trying
value "sFOLf (And True True)"
Alfio pointed out section 2.5.6 of the tutorial, page 19:
This archive was generated by a fusion of
Pipermail (Mailman edition) and