From e8e57dcb152e19bd7f64f5396d43ef35f270cf2e Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 2 Jun 2017 18:09:10 -0400 Subject: [PATCH] feat(init/meta/interactive): change at tactic addresses #1641 --- library/init/meta/interactive.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 9abfc8015c..c0fa4b0488 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -147,8 +147,15 @@ This tactic applies to any goal. `change U` replaces the main goal target `T` wi providing that `U` is well-formed with respect to the main goal local context, and `T` and `U` are definitionally equal. -/ -meta def change (q : parse texpr) : tactic unit := -i_to_expr q >>= tactic.change +meta def change (q : parse texpr) : parse location → tactic unit +| [] := i_to_expr q >>= tactic.change +| [h] := + do num_reverted : ℕ ← get_local h >>= revert, + expr.pi n bi d b ← target, + e ← i_to_expr q, + tactic.change $ expr.pi n bi e b, + intron num_reverted +| _ := fail "change does not support multiple locations" /-- This tactic applies to any goal. It gives directly the exact proof