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

chore: cleanup depArrow

Browse source 
Cleanup hack used before we implemented: parsers have precedence not tokens
This commit is contained in:
Leonardo de Moura 2020-11-14 07:00:10 -08:00
parent 9c6c568caf
commit 155c377bc6
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -91,8 +91,8 @@ It is feasible to support dependent arrows such as `{α} → α → α` without
Here is the encoding:
```
def implicitShortBinder := node `Lean.Parser.Term.implicitBinder $ "{" >> many1 binderIdent >> pushNone >> "}"
def depArrowShortPrefix := try (implicitShortBinder >> checkPrec 25 >> unicodeSymbol " → " " -> ")
def depArrowLongPrefix := bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> "
def depArrowShortPrefix := try (implicitShortBinder >> unicodeSymbol " → " " -> ")
def depArrowLongPrefix := bracketedBinder true >> unicodeSymbol " → " " -> "
def depArrowPrefix := depArrowShortPrefix <|> depArrowLongPrefix
@[builtinTermParser] def depArrow := parser! depArrowPrefix >> termParser
```
@ -100,7 +100,7 @@ Note that no changes in the elaborator are needed.
We decided to not use it because terms such as `{α} → α → α` may look too cryptic.
Note that we did not add a `explicitShortBinder` parser since `(α) → α → α` is really cryptic as a short for `(α : Type) → α → α`.
-/
@[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
@[builtinTermParser] def depArrow := parser!:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
def simpleBinder := parser! many1 binderIdent >> optType
@[builtinTermParser]