[isabelle-dev] unhelpful low-level error message from primrec
krauss at in.tum.de
Sun May 22 19:36:30 CEST 2011
> I just noticed this error message from primrec if you write a
> specification that is not primitive recursive. Here is a simplified
> 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
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...
More information about the isabelle-dev