Email Gateway (Aug 22 2022 at 11:53): Email Gateway (Aug 22 2022 at 11:53):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have a fairly large recursive function (~160 lines) that is causing
problems, in when I try to get Isabelle to accept the function
definition (using either the fun or function keyword) I am getting the
following output:
* exception THM 0 raised (line 705 of "thm.ML"):
* implies_elim: major premise
followed by what looks like a lengthy internal proof state of some
sort from the function package. I have stepped through the function
commenting out chunks of code and putting "undefined" everywhere, and
it appears that the problem is in the final recursive call at the
bottom of my definition.
How can I work around this other than trying to split my function up,
or begin to try to find out what the problem is? The error message is
not very helpful in working out where the problem lies. Is there a
known common cause for this exception when defining functions?
Many thanks,
Dominic
Email Gateway (Aug 22 2022 at 12:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominic,
I think the best what can be done at the moment is to provide a minimal
example here on the mailing list.
All the best,
Florian
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC