[isabelle-dev] unhelpful low-level error message from primrec
brianh at cs.pdx.edu
Sun May 22 00:12:59 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.
It might be nice to generate a more helpful error message in this
case, instead of one that originates from a lower-level tool.
More information about the isabelle-dev