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

feat: simplify termination_by new syntax

Browse source 
We don't need `using` anymore since we are going to use TC inference.
This commit is contained in:
Leonardo de Moura 2022-01-12 06:18:11 -08:00
parent 1a6abe1dad
commit a1ab5c0ccb
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -34,8 +34,7 @@ def terminationByCore := leading_parser "termination_by' " >> terminationHint te
def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq
def terminationByElement := leading_parser ppLine >> many (ident <|> "_") >> " => " >> termParser >> optional ";"
def terminationByComponent := leading_parser many1Indent terminationByElement >> optional (ppLine >> " using " >> termParser)
def terminationBy := leading_parser ppLine >> "termination_by " >> many terminationByComponent
def terminationBy := leading_parser ppLine >> "termination_by " >> many1Indent terminationByElement
def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy