Re: [isabelle] simp matching depends on lexicographic variable naming
On 2/13/2013 3:21 AM, Tobias Nipkow wrote:
Such a tool is in the making. For the time being you can prefix your
"apply simp" by "using [[simp_trace]]". This gives you a very detailed
trace, probably much more than what you want.
No, "using [[simp_trace]]" works perfect for simple test cases. Using a
fancy debugger wouldn't be any easier. Figuring out where to set the
break points for a debugger can be no easy task, not I've used a
debugger much, or any, because it's easier to just print to screen, and
then prompt the user, than learn how to use a debugger.
So reducing a formula down more and more can serve the purpose of single
stepping or setting break points.
But, I was wanting to confirm whether this sentence, page 178,
"Permutative rewrite rules can be turned into simplication rules in
the usual manner via the simp attribute; the simplifer recognizes
their special status automatically."
means it does the permutative rewrite rules first, and it does mean
that. The commutative and left-commutative rules end up doing together
what I had as one rule.
This archive was generated by a fusion of
Pipermail (Mailman edition) and