diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index d932aec302..7c499a279a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -177,6 +177,12 @@ that have not been fixed by type inference or type class resolution. meta def eapply (q : parse texpr) : tactic unit := i_to_expr_for_apply q >>= tactic.eapply +/-- +Similar to the `apply` tactic, but allows the user to provide a `apply_cfg` configuration object. +-/ +meta def apply_with (q : parse qexpr) (cfg : apply_cfg) : tactic unit := +do e ← i_to_expr_for_apply q, tactic.apply e cfg + /-- This tactic tries to close the main goal `... |- U` using type class resolution. It succeeds if it generates a term of type `U` using type class resolution. diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 9863d414ee..2d3d6927ff 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -832,7 +832,9 @@ private meta def try_apply_opt_auto_param (cfg : apply_cfg) (ms : list expr) : t when (cfg.auto_param || cfg.opt_param) $ mwhen (has_opt_auto_param ms) $ do gs ← get_goals, - ms.mfor' (λ m, set_goals [m] >> try apply_opt_param >> try apply_auto_param), + ms.mfor' (λ m, set_goals [m] >> + when cfg.opt_param (try apply_opt_param) >> + when cfg.auto_param (try apply_auto_param)), set_goals gs meta def apply (e : expr) (cfg : apply_cfg := {}) : tactic unit := diff --git a/tests/lean/apply_tac.lean b/tests/lean/apply_tac.lean index f991cfc046..bf1a7c738d 100644 --- a/tests/lean/apply_tac.lean +++ b/tests/lean/apply_tac.lean @@ -56,7 +56,7 @@ eq.trans h₁ h₂ example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c := begin - apply foo h₁ -- uses auto_param for solving goal + apply @foo a b c h₁ -- uses auto_param for solving goal end lemma my_div_self (a : nat) (h : a ≠ 0 . assumption) : a / a = 1 := @@ -66,3 +66,29 @@ example (a : nat) (h : a ≠ 0) : a / a = 1 := begin apply my_div_self -- uses auto_param for solving goal end + +example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c := +begin + apply_with (@foo a b c h₁) {auto_param := ff}, + assumption +end + +example (a : nat) (h : a ≠ 0) : a / a = 1 := +begin + apply_with my_div_self {auto_param := ff}, + assumption +end + +example (a : nat) (h : a ≠ 0) : a / a = 1 := +begin + apply_with my_div_self {opt_param := ff} -- uses auto_param for solving goal +end + +def bla2 : nat := +begin + apply_with f {opt_param := ff}, + exact 20 +end + +example : bla2 = 21 := +rfl