From 2ff8052ce46cd4aa76edf6a969e8ea69077b710a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Apr 2021 19:40:40 -0700
Subject: [PATCH] fix: missing `do`

---
 src/Lean/Elab/BuiltinNotation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index c986d185a1..df6c4f2432 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -255,7 +255,7 @@ where
      | some (α, lhs, rhs) =>
        let mut lhs := lhs
        let mut rhs := rhs
-       let mkMotive (typeWithLooseBVar : Expr) :=
+       let mkMotive (typeWithLooseBVar : Expr) := do
          withLocalDeclD (← mkFreshUserName `x) α fun x => do
            mkLambdaFVars #[x] $ typeWithLooseBVar.instantiate1 x
        let mut expectedAbst ← kabstract expectedType rhs