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

feat: add structInstLVal

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-02 17:30:36 -08:00
parent 2abfa1bcff
commit cdb7e0cfae
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Parser/Term.lean
View file

@ -58,7 +58,9 @@ def haveAssign := parser! " := " >> termParser
@[builtinTermParser] def «suffices» := parser! "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
@[builtinTermParser] def «show» := parser! "show " >> termParser >> fromTerm
@[builtinTermParser] def «fun» := parser! unicodeSymbol "λ" "fun" >> many1 (termParser appPrec) >> darrow >> termParser
def structInstField := parser! ident >> " := " >> termParser
def structInstArrayRef := parser! symbol "[" (appPrec+1) >> termParser >>"]"
def structInstLVal := (ident <|> structInstArrayRef) >> many (("." >> ident) <|> structInstArrayRef)
def structInstField := parser! structInstLVal >> " := " >> termParser
def structInstSource := parser! ".." >> optional termParser
@[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (ident >> " . ")) >> sepBy (structInstField <|> structInstSource) ", " true >> "}"
def typeSpec := parser! " : " >> termParser