chore: make 'while' available earlier (leanprover#5784)

src/Init.lean

@@ -35,3 +35,4 @@ import Init.Ext
 import Init.Omega
 import Init.MacroTrace
 import Init.Grind
+import Init.While

src/Init/NotationExtra.lean

@@ -10,6 +10,7 @@ import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
 import Init.Conv
 import Init.Meta
+import Init.While
 
 namespace Lean
 
@@ -344,42 +345,6 @@ syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " t
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
-/-! # `repeat` and `while` notation -/
-
-inductive Loop where
-  | mk
-
-@[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
-    match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
-
-instance : ForIn m Loop Unit where
-  forIn := Loop.forIn
-
-syntax "repeat " doSeq : doElem
-
-macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
-
-syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
-
-syntax "while " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
-
-syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
-
-macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
-
 macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 

src/Init/While.lean

@@ -0,0 +1,51 @@
+/-
+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.Core
+
+/-!
+# Notation for `while` and `repeat` loops.
+-/
+
+namespace Lean
+
+/-! # `repeat` and `while` notation -/
+
+inductive Loop where
+  | mk
+
+@[inline]
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
+    match ← f () b with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
+
+instance : ForIn m Loop Unit where
+  forIn := Loop.forIn
+
+syntax "repeat " doSeq : doElem
+
+macro_rules
+  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+
+syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
+
+syntax "while " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
+
+macro_rules
+  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+
+end Lean