From ba41dad9a40125f7bb1cc5bd8149caa44d2d0c55 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2020 16:53:25 -0700 Subject: [PATCH] feat: add `evalFocus` --- src/Lean/Elab/Tactic/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 9157c8fcab..bf350e23dd 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -253,6 +253,9 @@ fun stx => (stx.getArg 0).forSepArgsM evalTactic @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic +@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := +fun stx => focus $ evalTactic (stx.getArg 1) + @[builtinTactic paren] def evalParen : Tactic := fun stx => evalSeq1 (stx.getArg 1)