Re: [isabelle] primrec with mutual recursion over nat
> 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"?
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)"
"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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and