Hi Brian,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: "nat => nat" where
"foo 0 = 1" | "foo (Suc n) = foo 0"
*** Extra variables on rhs: "foo"
*** The error(s) above occurred in definition "foo_def":
*** "foo \<equiv> \<lambda>a. nat_rec 1 (\<lambda>n na. foo 0) a"
*** At command "primrec"
Apparently, the primrec package gets as far as trying to register the
non-recursive definition; then the definition command fails, and the
error is not caught by primrec.
This is a regular source of confusion for newbies, and I want to see
this improved for a long time. IIRC, the problem is that the primrec
schema is not so easy to check (in the presence of mutual/nested types
etc.), and thus the package simply defers that check to the lower level
layers. Catching the low-level error and assuming that it is due to a
violation of the primrec schema is not really a good alternative, since
more serious confusion will arise in cases where that assumption does
not hold...
If anybody wants to investigate this in detail, and work out what the
missing check should look like, I'll be happy to look at patches...
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
