mathlib3 documentation

tactic.simpa

source
meta def tactic.interactive.simpa (use_iota_eqn : interactive.parse (optional (lean.parser.tk "!"))) (trace_lemmas : interactive.parse (optional (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 (optional (lean.parser.tk "using" *> interactive.types.texpr))) (cfg : 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, trace_lemmas := bool.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.

source
def tactic_doc.tactic.simpa  :
tactic_doc_entry

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.