diff --git a/src/Init/Lean/Elab.lean b/src/Init/Lean/Elab.lean
index 3944e01371..398d392899 100644
--- a/src/Init/Lean/Elab.lean
+++ b/src/Init/Lean/Elab.lean
@@ -18,3 +18,4 @@ import Init.Lean.Elab.Declaration
 import Init.Lean.Elab.Tactic
 import Init.Lean.Elab.Syntax
 import Init.Lean.Elab.Match
+import Init.Lean.Elab.DoNotation
diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index eaa1c49092..2179e2e9db 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -11,12 +11,6 @@ namespace Lean
 namespace Elab
 namespace Term
 
-@[builtinTermElab «do»] def elabDo : TermElab :=
-adaptExpander $ fun stx => match_syntax stx with
--- TODO: implement more than the bare minimum necessary for the paper example
-| `(do $x:ident ← $e:term; $f:term) => `(HasBind.bind $e (fun $x:ident => $f:term))
-| _                                 => throwUnsupportedSyntax
-
 @[builtinMacro Lean.Parser.Term.dollar] def expandDollar : Macro :=
 fun stx => match_syntax stx with
 | `($f $args* $ $a) => let args := args.push a; `($f $args*)
diff --git a/src/Init/Lean/Elab/DoNotation.lean b/src/Init/Lean/Elab/DoNotation.lean
new file mode 100644
index 0000000000..af8d83213d
--- /dev/null
+++ b/src/Init/Lean/Elab/DoNotation.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Term
+import Init.Lean.Elab.Quotation
+
+namespace Lean
+namespace Elab
+namespace Term
+
+@[builtinTermElab «do»] def elabDo : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+-- TODO: implement more than the bare minimum necessary for the paper example
+| `(do $x:ident ← $e:term; $f:term) => `(HasBind.bind $e (fun $x:ident => $f:term))
+| _                                 => throwUnsupportedSyntax
+
+end Term
+end Elab
+end Lean