Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
On 18.01.2013 05:35, Gottfried Barrow wrote:
primrec sFOLf :: "sFOLdt => bool" where
"sFOLf (In u1 u2) = (u1 inS u2)" |
"sFOLf (And f1 f2) = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" |
"sFOLf (Rec f) = True"
This definition is not primitive recursive and hence rejected by primrec
(recursive calls my only make the arguments structurally smaller, so
"sFOLf (Rec f1)" is not valid on the rhs.
This archive was generated by a fusion of
Pipermail (Mailman edition) and