[isabelle] simple question



Hello all,

The function 'f' (above) does not work, returning the fallowing message.
I'd like to know what's wrong in this definition.

typedecl sbf

datatype frm = At sbf | Nt frm

consts
  f :: "frm => frm"
  primrec
    "f (At x) = At x"
    "f (Nt x) = Nt(x)"
    "f (Nt(Nt x)) = f (x)"

*** Primrec definition error:
*** illegal argument in pattern
*** in
*** "f (Nt (Nt x)) = f x"
*** At command "primrec".

Thank you,
Lucas Cavalcante




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