refactor: move elabDo to its own file

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

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*)

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