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

feat: allow arbitrary terms after @

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-11 08:59:17 -08:00
parent c7551b5474
commit a276b59a80
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/Term.lean
View file

@ -69,7 +69,7 @@ def optType : Parser := optional typeSpec
@[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}"
@[builtinTermParser] def listLit := parser! symbol "[" appPrec >> sepBy termParser "," true >> "]"
@[builtinTermParser] def arrayLit := parser! symbol "#[" appPrec >> sepBy termParser "," true >> "]"
@[builtinTermParser] def explicit := parser! symbol "@" appPrec >> id
@[builtinTermParser] def explicit := parser! symbol "@" appPrec >> termParser appPrec
@[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)