From 2e6ac0cd6173caeefc25d9c1b084e2a03d93ac53 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jan 2020 18:15:27 -0800
Subject: [PATCH] feat: eval `paren` tactic

---
 src/Init/Lean/Elab/Tactic/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index e2e8e654e9..592cee455c 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -280,6 +280,9 @@ fun stx => match_syntax stx with
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic paren] def evalParen : Tactic :=
+fun stx => evalTactic (stx.getArg 1)
+
 @[builtinTactic nestedTacticBlock] def evalNestedTacticBlock : Tactic :=
 fun stx => focus stx (evalTactic (stx.getArg 1))