Re: [isabelle] Help with simplification loops.



> 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.

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.