max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add terminationByCore parser

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-11 14:44:36 -08:00
parent ca89da28d0
commit ce76ad44ea
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Command.lean
View file

@ -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