Re: [isabelle] primrec
Thank you all for the quick answers.
I will use "fun". I was afraid that using fun
would require providing the well founded
relation which ensures termination.
However it seems that in this case Isabelle
figures it out automatically.
On 11/09/2011 10:39 AM, Lukas Bulwahn wrote:
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