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.

  -- Lars





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