Email Gateway (Aug 22 2022 at 12:43): Email Gateway (Aug 22 2022 at 12:43):From: "henning.seidler" <henning.seidler@mailbox.tu-berlin.de>
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
signature.asc
Email Gateway (Aug 22 2022 at 12:43):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Henning,
The error message is misleading. If you try with a "new-style nat", you get a more informative message:
datatype nat = Z | Suc nat
primrec foo:: "('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a" and bar:: "('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a" where
"foo f Z a = a"
| "foo f (Suc n) a = f (bar f n a)"
| "bar f Z b = b"
| "bar f (Suc n) b = f (foo f n b)"
produces
"Scratch.nat" is neither mutually recursive with "Scratch.nat" nor nested recursive through itself
The definition works fine if you use "fun" instead. Where did you read that "this works fine with new-style datatypes"? I'm not aware of any sentence to that effect in "datatypes.pdf" -- but maybe I'm wrong.
Cheers,
Jasmin
Last updated: Apr 23 2024 at 08:19 UTC