Email Gateway (Aug 22 2022 at 21:02): Email Gateway (Aug 22 2022 at 21:02):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear all,
I've run into a problem where the case translation, which converts input syntax of the
form "case x of ... => ... | ... => ..." into case combinators, produces a TYPE exception
with the message "illegal schematic variable". A small example can be found in the
attached theory. (The first term statement parses and displays the term as usual, but the
second statement produces the above error.)
Interestingly, the problem occurs only if the datatype declaration inside the locale comes
only after the function definition in the locale. Has anyone an idea what's happening here?
Best,
Andreas
Scratch.thy
Last updated: Apr 26 2024 at 20:16 UTC