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

`People can ignore what I was talking about, unless someone wants to give
``me a complete "datatype" and "fun/primrec" solution based on the
``informal, recursive definition I gave. Or a solution of another form
``would be okay.
`
Trying to figure out how recursion works, I have this experimental code:
typedecl sT
consts inS :: "sT => sT => bool" (infixl "inS" 55)
datatype sFOLdt =
In sT sT
|And bool bool
|Rec bool
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"
which gives the error: Extra variables on rhs: "(sFOLf::(sFOLdt => bool))"

`All that to say, trial and error has shown me I haven't understood
``certain basic things, but trial and error can be an excellent learning
``aid sometimes.
`
Regards,
GB

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