Re: [isabelle] simple question



Hi Lucas,

I am not sure what you are trying to do but I think you have to rethink the definition of your datatype.

I took the liberty to modify it a bit and here is an alternative definition:

datatype frm = At sbf | Nt frm | Nts frm;

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

I hope it helps.

George

lucas cavalcante wrote:
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.