From e7d818fe61253d207f2ca4e2c371d0a63c0f1d73 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2019 16:26:34 -0800 Subject: [PATCH] chore: add workaround for attribute parsing infrastructure --- src/Init/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 2bdab9d11c..a45a635762 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -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