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

feat: allow _ "else case" at inductionAlt

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-22 11:16:20 -08:00
parent 14b9e13dc1
commit 4a8c192a00
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Tactic.lean
View file

@ -38,7 +38,7 @@ def ident' : Parser := ident <|> underscore
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident
def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident >> many ident >> darrow >> termParser
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident >> darrow >> termParser
def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
def withAlts : Parser := optional (" with " >> inductionAlts)
def usingRec : Parser := optional (" using " >> ident)