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:
consts inS :: "sT => sT => bool" (infixl "inS" 55)
datatype sFOLdt =
In sT sT
|And bool 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and