feat: helper parser for issue #1371

leanprover · Jul 31, 2022 · 2f00d60 · 2f00d60
1 parent cc03244
commit 2f00d60
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
@@ -284,6 +284,12 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 
 @[builtinTermParser] def defaultOrOfNonempty   := leading_parser "default_or_ofNonempty% " >> optional "unsafe"
 
+/--
+Helper parser for marking `match`-alternatives that should not trigger errors if unused.
+We use them to implement `macro_rules` and `elab_rules`
+-/
+@[builtinTermParser] def noErrorIfUnused := leading_parser "no_error_if_unused%" >> termParser
+
 def namedArgument  := leading_parser (withAnonymousAntiquot := false) atomic ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := leading_parser (withAnonymousAntiquot := false) ".."
 def argument       :=