def
conv.interactive.dsimp
:
interactive.parse interactive.types.only_flag → interactive.parse tactic.simp_arg_list → interactive.parse interactive.types.with_ident_list → (tactic.dsimp_config := {md := tactic.transparency.reducible, max_steps := simp.default_max_steps, canonize_instances := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, eta := bool.tt, zeta := bool.tt, beta := bool.tt, proj := bool.tt, iota := bool.tt, unfold_reducible := bool.ff, memoize := bool.tt}) → conv unit
def
conv.interactive.simp
:
interactive.parse interactive.types.only_flag → interactive.parse tactic.simp_arg_list → interactive.parse interactive.types.with_ident_list → (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}) → conv unit
def
conv.interactive.rewrite
:
interactive.parse tactic.interactive.rw_rules → (tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) → conv unit
def
conv.interactive.rw
:
interactive.parse tactic.interactive.rw_rules → (tactic.rewrite_cfg := {to_apply_cfg := {md := tactic.transparency.reducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}, symm := bool.ff, occs := occurrences.all}) → conv unit