def
tactic.interactive.simpa
:
interactive.parse (optional (lean.parser.tk "!")) → interactive.parse interactive.types.only_flag → interactive.parse tactic.simp_arg_list → interactive.parse interactive.types.with_ident_list → interactive.parse (optional (lean.parser.tk "using" *> interactive.types.texpr)) → (tactic.simp_config_ext := {to_simp_config := {max_steps := simp.default_max_steps, contextual := bool.ff, lift_eq := bool.tt, canonize_instances := bool.tt, canonize_proofs := bool.ff, use_axioms := bool.tt, zeta := bool.tt, beta := bool.tt, eta := bool.tt, proj := bool.tt, iota := bool.tt, iota_eqn := bool.ff, constructor_eq := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, memoize := bool.tt}, discharger := tactic.failed unit}) → tactic unit
This is a "finishing" tactic modification of simp. It has two forms.
simpa [rules, ...] using ewill simplify the goal and the type ofeusingrules, then try to close the goal usinge.Simplifying the type of
emakes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.simpa [rules, ...]will simplify the goal and the type of a hypothesisthisif present in the context, then try to close the goal using theassumptiontactic.