simp discharge function using the given tactic syntax code.
simp dischargers are in
SimpM which does not have access to
We need access to
Term.State to store messages and update the info tree.
Thus, we create an
IO.ref to track these changes at
Term.State when we execute
We must set this reference with the current
Term.State before we execute
simp using the
Elaborate extra simp theorems provided to
stx is of the form
"[" simpTheorem,* "]"
eraseLocal == true, then we consider local declarations when resolving names for erased theorems (
this option only makes sense for
* is used.
simpLocation ctx discharge? varIdToLemmaId loc
runs the simplifier at locations specified by
using the simp theorems collected in
optionally running a discharger specified in
discharge? on generated subgoals.
For many tactics other than the simplifier,
one should use the
withLocation tactic combinator
when working with a