[isabelle] primrec


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?

Using fun instead of primrec seem to solve the problem,
but fun seems more general.

Best regards,

Viorel Preoteasa

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