Re: [isabelle] primrec
On 11/09/2011 09:21 AM, Viorel Preoteasa wrote:
The error message might be misleading, but this function is not
in the third equation, you would only be allowed to use recursive calls
Special x and Special y, but not Special v.
I have the following definitions:
datatype Tree =
leaf1 | leaf2 | "tree" "Tree" "Tree" (infixr ".." 65)
primrec Special :: "Tree => bool" where
"Special leaf1 = True" |
"Special leaf2 = True" |
"Special (x .. y) = (case x of leaf1 => Special y | leaf2 => Special y
| (u .. v) ⇒ u = leaf1 /\ Special y /\ (Special v))"
On the definition of Special I get the error:
Extra variables on rhs: "Special"
The error(s) above occurred in definition "Special_def"
How could Special be an extra variable? Is it possible
to fix this definition?
One can probably reformulate it to fit the syntactic criteria of
primrec, but it certainly easier just to use fun, as Larry suggested.
This archive was generated by a fusion of
Pipermail (Mailman edition) and