mathlib documentation

tactic.simpa

source
meta def tactic.interactive.simpa (use_iota_eqn : interactive.parse (lean.parser.tk "!")?) (trace_lemmas : interactive.parse (lean.parser.tk "?")?) (no_dflt : interactive.parse interactive.types.only_flag) (hs : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (tgt : interactive.parse (lean.parser.tk "using" *> interactive.types.texpr)?) (cfg : tactic.simp_config_ext := {to_simp_config := {max_steps := simp.default_max_steps, contextual := ff, lift_eq := tt, canonize_instances := tt, canonize_proofs := ff, use_axioms := tt, zeta := tt, beta := tt, eta := tt, proj := tt, iota := tt, iota_eqn := ff, constructor_eq := tt, single_pass := ff, fail_if_unchanged := tt, memoize := tt, trace_lemmas := ff}, discharger := tactic.failed unit}) :
tactic unit

This is a "finishing" tactic modification of simp. It has two forms.

  • simpa [rules, ...] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

    Simplifying the type of e makes 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 hypothesis this if present in the context, then try to close the goal using the assumption tactic.