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

feat: add have-by and show-by syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-14 14:25:35 -07:00
parent fc4ab139b5
commit f95675dc22
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Parser/Term.lean
View file

@ -45,6 +45,8 @@ def leadPrec := maxPrec - 1
/- Built-in parsers -/
@[builtinTermParser] def byTactic := parser!:maxPrec "by " >> Tactic.indentedNonEmptySeq
-- `checkPrec` necessary for the pretty printer
@[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
@[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit
@ -67,11 +69,11 @@ def optIdent : Parser := optional (try (ident >> " : "))
@[builtinTermParser] def «if» := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm)
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
def sufficesDecl := optIdent >> termParser >> fromTerm
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> fromTerm
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := parser! structInstLVal >> " := " >> termParser
@ -242,8 +244,6 @@ stx.isAntiquot || stx.isIdent
@[builtinTermParser] def seqRight := tparser! infixR " *> " 60
@[builtinTermParser] def map := tparser! infixR " <$> " 100
@[builtinTermParser] def byTactic := parser!:maxPrec "by " >> Tactic.indentedNonEmptySeq
@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot funBinder >> ")"
@[builtinTermParser] def panic := parser!:leadPrec "panic! " >> termParser