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.


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