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

chore: add missing ppSpace

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-30 11:17:53 -08:00
parent 4c43f76b2a
commit 6aab25b3cc
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -175,7 +175,7 @@ def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
@[builtinTermParser] def noindex := parser! "noindex!" >> termParser maxPrec
@[builtinTermParser] def binrel := parser! "binrel!" >> ident >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binrel := parser! "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := parser! "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser

2
tests/lean/macroStack.lean.expected.out
View file

@ -1,7 +1,7 @@
macroStack.lean:4:5: error: unknown identifier 'x'
macroStack.lean:8:6: error: unknown identifier 'x'
with resulting expansion
binrel! Greater✝x 0
binrel! Greater✝ x 0
while expanding
x > 0
while expanding