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

feat: add change tactic parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-29 08:09:39 -07:00
parent 0288ed0129
commit af86cc801d
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -39,7 +39,11 @@ def ident' : Parser := ident <|> underscore
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 51 >> " = " >> ident
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional (try (ident >> " : ")) >> termParser 51 >> " = " >> ident
def location : Parser := "at " >> ("*" <|> (many ident >> optional (unicodeSymbol "⊢" "|-")))
@[builtinTacticParser] def change := parser! nonReservedSymbol "change " >> termParser >> optional location
@[builtinTacticParser] def changeWith := parser! nonReservedSymbol "change " >> termParser >> " with " >> termParser >> optional location
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
def holeOrTactic := Term.hole <|> Term.namedHole <|> tacticParser
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> holeOrTactic