[isabelle] primrec with mutual recursion over nat



Hello,

I want to define two mutual recursive functions, that both get a natural
number as an argument.
The tutorial for datatypes states that this works fine with new-style
datatypes, but in my case I get the error:
"nat" is an old-style datatype

Some minimal example would be:
primrec foo:: "('a â 'a) â nat â 'a â 'a" and bar:: "('a â 'a) â nat â
'a â 'a" where
  "foo f 0 a = a"
| "foo f (Suc n) a = f (bar f n a)"
| "bar f 0 b = b"
| "bar f (Suc n) b = f (foo f n b)"

Is there some way to fix this problem? Is there some "new-style nat"?

Regards,
Henning

Attachment: signature.asc
Description: OpenPGP digital signature



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