Email Gateway (Nov 14 2021 at 13:49): Email Gateway (Nov 14 2021 at 13:49):From: Makarius <makarius@sketis.net>
On 14/11/2021 01:38, Peter Lammich wrote:
I'm getting an exception
exception Fail raised (line 673 of "variable.ML"): Bad context: clash
of fresh free for bound: :001 vs. xbI'm lost! Can someone please explain what might go wrong here, and how
to debug and track down such errors, or point me to (ideally concise
and understandable) documentation about what 'context discipline'
exactly means.
Here is the announcement of the NEWS item on isabelle-dev some weeks ago:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2021-October/017512.html
I had spent several days looking carefully at old (and some new) tools that
where violating the plain block structure that the Proof.context discipline
formalizes.
In the end it did work reasonably well: So an ancient warning could become a
proper error.
val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt
goal_t) (fn _ => tac)
Do you see a chance to work with proper Goal.prove, instead of the internal
side-entry Goal.prove_internal?
Makarius
Email Gateway (Nov 14 2021 at 13:52):From: Makarius <makarius@sketis.net>
You can use get_simpset / put_simpset to produce an augmented simpset before
going into the context. Here is an example where I did have a performance leak
beforehand:
https://isabelle-dev.sketis.net/rISABELLE71bafd70acb
Makarius
Last updated: Jan 04 2025 at 20:18 UTC