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

feat: add induction tactic parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-20 13:09:40 -08:00
parent bc4b3047a9
commit 2fee8059b6
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/lean4-syntax.el
View file

@ -17,7 +17,7 @@
"match_syntax" "match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"end" "this" "using" "using_well_founded" "namespace" "section"
"attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
"attributes" "raw" "replacing"
"attributes" "raw" "replacing" "generalizing"
"calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
"exists" "if" "then" "else" "assume" "from" "init_quot"
"mutual" "def" "run_cmd")

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

@ -36,7 +36,13 @@ def ident' : Parser := ident <|> underscore
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticParser
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
def majorPremise := parser! optional (try (ident >> " : ")) >> 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)
def generalizingVars := optional (" generalizing " >> many1 ident)
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"