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

chore: add workaround for attribute parsing infrastructure

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-11 16:26:34 -08:00
parent 8fd70ee882
commit e7d818fe61
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

@ -169,7 +169,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
@[builtinTermParser] def orM := tparser! infixR " <||> " 30
@[builtinTermParser] def andM := tparser! infixR " <&&> " 35
@[builtinTermParser] def andthen := tparser! infixR " >> " 60
@[builtinTermParser] def bind := tparser! infixR " >>= " 55
@[builtinTermParser] def bindOp := tparser! infixR " >>= " 55
@[builtinTermParser] def mapRev := tparser! infixR " <&> " 100
@[builtinTermParser] def seq := tparser! infixL " <*> " 60
@[builtinTermParser] def seqLeft := tparser! infixL " <* " 60