[isabelle] simple question
The function 'f' (above) does not work, returning the fallowing message.
I'd like to know what's wrong in this definition.
datatype frm = At sbf | Nt frm
f :: "frm => frm"
"f (At x) = At x"
"f (Nt x) = Nt(x)"
"f (Nt(Nt x)) = f (x)"
*** Primrec definition error:
*** illegal argument in pattern
*** "f (Nt (Nt x)) = f x"
*** At command "primrec".
This archive was generated by a fusion of
Pipermail (Mailman edition) and