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 \lambdaa. nat_rec 1 (\lambdan 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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
