From fba1571fdf0a6ddc0bd04e600691ca9e7b8b83fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2020 15:26:35 -0700 Subject: [PATCH] chore: add `evalSeq1` --- src/Lean/Elab/Tactic/Basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 41221fcb73..6bad41ac85 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -246,8 +246,10 @@ modifyMCtx fun mctx => @[builtinTactic seq] def evalSeq : Tactic := fun stx => (stx.getArg 0).forSepArgsM evalTactic +@[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq + @[builtinTactic paren] def evalParen : Tactic := -fun stx => evalTactic (stx.getArg 1) +fun stx => evalSeq1 (stx.getArg 1) @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic