Hello all, 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. It might be nice to generate a more helpful error message in this case, instead of one that originates from a lower-level tool. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
