Ideas for simp trace
Jump to navigation
Jump to search
- click on a symbol in the resulting term and trace back which rewrite rules where used to generate this symbol
- click on a subterm of the start term to jump to the place where it is rewritten
- which rewrite rules where used to /remove/ a assumption (often assumptions get removed which are then missing for the arith tactics)
- why is certain conditional rewrite rule not applied, look at the simp trace of its conditions
- in addition to "certain conditional rewrite rule": rewrite rules from specific theories (or rule sets like ring_simps)
- which rewrite rules failed to apply at a particular intermediate step (perhaps also filtered by theories)
- a option to get after a (successful) simp the set of rewrite rules that were applied, such that if I were to do (simp only: that_set), the command would get the same result. (similar to sledgehammer)
- in the same spirit: report rules that have been added explicitly (via "add:" or "using", if this is possible to detect) but not used
- search the trace for a particular rule