From cec66bc75cc5472148afce4ee881ee28fa0177c8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 08:21:49 -0800
Subject: [PATCH] feat: add a few helper tactics

---
 src/Init/Lean/Parser/Tactic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index be7b7f37e4..6b33673faf 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -43,6 +43,12 @@ 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 «try»        := parser! nonReservedSymbol "try " >> tacticParser
+@[builtinTacticParser] def «repeat»     := parser! nonReservedSymbol "repeat " >> tacticParser
+@[builtinTacticParser] def «allGoals»   := parser! nonReservedSymbol "allGoals " >> tacticParser
+@[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
+@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
+
 @[builtinTacticParser] def paren        := parser! "(" >> seq >> ")"
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"