From 61d4290fa84604b8bf0c309563afe4fcf6e063e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 18:00:48 -0800 Subject: [PATCH] feat: add `paren` --- src/Init/Lean/Parser/Tactic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean index 3cc4c8fc6e..be7b7f37e4 100644 --- a/src/Init/Lean/Parser/Tactic.lean +++ b/src/Init/Lean/Parser/Tactic.lean @@ -43,6 +43,7 @@ def seq := parser! sepBy tacticParser "; " true @[builtinTacticParser] def «exact» := parser! nonReservedSymbol "exact " >> termParser @[builtinTacticParser] def «refine» := parser! nonReservedSymbol "refine " >> termParser @[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> tacticParser +@[builtinTacticParser] def paren := parser! "(" >> seq >> ")" @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end" @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}" @[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1