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

feat: add helper parsers for auto-completion

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-01 21:17:57 -07:00
parent 8d00a06d97
commit caae7952cd
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -204,6 +204,7 @@ def argument :=
@[builtinTermParser] def app := trailing_parser:leadPrec:maxPrec many1 argument
@[builtinTermParser] def proj := trailing_parser checkNoWsBefore >> "." >> (fieldIdx <|> ident)
@[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
@[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
@[builtinTermParser] def arrow := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@ -215,6 +216,7 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> (fieldIdx <|> ident) >> many argument
@[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "