From ce76ad44ea8a21781284e8110be8e2f45a68b524 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Jan 2022 14:44:36 -0800 Subject: [PATCH] feat: add `terminationByCore` parser --- src/Lean/Parser/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index fec4f33a7c..c3100e0296 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -31,9 +31,10 @@ def terminationHint1 (p : Parser) := leading_parser p def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p def terminationBy := leading_parser "termination_by " >> terminationHint termParser +def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq -def terminationSuffix := optional terminationBy >> optional decreasingBy +def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy @[builtinCommandParser] def moduleDoc := leading_parser ppDedent $ "/-!" >> commentBody >> ppLine