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

chore: prepare to move tactic match parser back to Lean/Parser/Tactic

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-22 06:52:41 -08:00
parent 1c31240ebb
commit a05ca020f4
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Parser/Tactic.lean
View file

@ -15,6 +15,11 @@ builtin_initialize
@[builtinTacticParser] def «unknown» := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq
def matchAltsTemp := Term.matchAlts (rhsParser := matchRhs)
@[builtinTacticParser low] def «matchTemp» := parser!:leadPrec "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAltsTemp
end Tactic
end Parser
end Lean