feat(init/control/coroutine): avoid mutual inductive

Reason: we want to delete the inductive compiler.

library/init/control/coroutine.lean

@@ -8,6 +8,10 @@ import init.control.monad init.wf init.control.reader
 
 universes u v w r s
 
+inductive coroutine_result_core (coroutine : Type (max u v w)) (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
+| done     {} : β → coroutine_result_core
+| yielded {}  : δ → coroutine → coroutine_result_core
+
 /--
    Asymmetric coroutines `coroutine α δ β` takes inputs of type `α`, yields elements of type `δ`,
    and produces an element of type `β`.
@@ -18,17 +22,16 @@ universes u v w r s
    to its caller, the relationship between them being similar to that between a called and
    a calling routine.
  -/
-mutual inductive coroutine, coroutine_result (α : Type u) (δ : Type v) (β : Type w)
-with coroutine : Type (max u v w)
-| mk    {} : (α → coroutine_result) → coroutine
-with coroutine_result : Type (max u v w)
-| done     {} : β → coroutine_result
-| yielded {}  : δ → coroutine → coroutine_result
+inductive coroutine (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
+| mk    {} : (α → coroutine_result_core coroutine α δ β) → coroutine
+
+abbreviation coroutine_result (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) :=
+coroutine_result_core (coroutine α δ β) α δ β
 
 namespace coroutine
 variables {α : Type u} {δ : Type v} {β γ : Type w}
 
-export coroutine_result (done yielded)
+export coroutine_result_core (done yielded)
 
 /-- `resume c a` resumes/invokes the coroutine `c` with input `a`. -/
 @[inline] def resume : coroutine α δ β → α → coroutine_result α δ β

library/init/control/coroutine_io.lean

@@ -13,7 +13,7 @@ universes u v w r s
 namespace coroutine_io
 variables {α δ β γ : Type}
 
-export coroutine_result_io (done yielded)
+export coroutine_result_core (done yielded)
 
 /-- `resume c a` resumes/invokes the coroutine_io `c` with input `a`. -/
 @[inline] def resume : coroutine_io α δ β → α → io (coroutine_result_io α δ β)

library/init/io.lean

@@ -5,7 +5,7 @@ Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich
 -/
 
 prelude
-import init.control.state init.control.except init.data.string.basic
+import init.control.state init.control.except init.data.string.basic init.control.coroutine
 import init.meta.tactic
 
 /-- Like https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
@@ -259,12 +259,10 @@ meta instance eio_unit.has_eval {ε : Type} [has_to_format ε] : has_eval (excep
   | except.error e := tactic.fail e
   | except.ok a    := pure ()⟩
 
-
 local attribute [reducible] io
 /-- A variant of `coroutine` on top of `io` -/
-mutual inductive coroutine_io, coroutine_result_io (α δ β: Type)
-with coroutine_io : Type
-| mk    {} : (α → io coroutine_result_io) → coroutine_io
-with coroutine_result_io : Type
-| done     {} : β → coroutine_result_io
-| yielded {}  : δ → coroutine_io → coroutine_result_io
+inductive coroutine_io (α δ β: Type) : Type
+| mk    {} : (α → io (coroutine_result_core.{0 0 0} coroutine_io α δ β)) → coroutine_io
+
+abbreviation coroutine_result_io (α δ β: Type) : Type :=
+coroutine_result_core.{0 0 0} (coroutine_io α δ β) α δ β