Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: John Ridgway <jridgway@wesleyan.edu>
Friends -
I realize this is a very general question, but I don't know how else
to get at what I want.
I'm having problems with simplification. It goes on forever (or
until I kill it) and when I turn on simplification tracing I can see
that I'm getting some kind of loop, but I cannot figure out which
rules are causing the loop. Is there some (probably obvious) way of
doing this?
Peace
Email Gateway (Aug 17 2022 at 14:14):From: nipkow@in.tum.de
It's like a nonterminating program, you have to figure it out yourself.
In the worst case by wading through the trace. Try setting
Isabelle -> Settings -> Trace Simplifier Depth
to some small number like 2, in which case it does not show all the nested
conditional rewrites but merely the "top level", which may help.
(Don't mind that PG always shows the same value for Trace Simplifier Depth,
it is changed internally).
Tobias
Last updated: May 03 2024 at 08:18 UTC