simp_result are a pair of tactics for
simp to the result produced by other tactics.
As examples, tactics which use
may insert additional
id terms in the result they produce.
If there is some reason these are undesirable
(e.g. the result term needs to be human-readable, or
satisfying syntactic rather than just definitional properties),
wrapping those tactics in
can remove the
id terms "after the fact".
Similarly, tactics using
rw will nearly always introduce
but sometimes these will be easy to remove,
for example by simplifying using
This is a non-definitional simplification lemma,
and so wrapping these tactics in
simp_result will result
in a definitionally different result.
There are several examples in the associated test file,
demonstrating these interactions with
These tactics should be used with some caution. You should consider whether there is any real need for the simplification of the result, and whether there is a more direct way of producing the result you wanted, before relying on these tactics.
Both are implemented in terms of a generic
which allows you to run an arbitrary tactic and modify the returned results.