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

chore: prepare to change structInst syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-20 13:57:52 -08:00
parent bb6945d384
commit 27e26998d2
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -70,7 +70,16 @@ def sufficesDecl := optIdent >> termParser >> (fromTerm <|> byTactic)
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := ppGroup $ parser! structInstLVal >> " := " >> termParser
@[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
@[builtinTermParser] def structInst := parser!
(checkInsideQuot >>
"{" >> ppHardSpace >> optional (atomic (termParser >> " with "))
>> manyIndent (group (structInstField >> optional ", "))
>> optional ".."
>> optional (" : " >> termParser) >> " }")
<|>
(checkOutsideQuot >>
"{" >> ppHardSpace >> optional (atomic (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }")
def typeSpec := parser! " : " >> termParser
def optType : Parser := optional typeSpec
@[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec