chore: update stage0

stage0/src/Init/Control/Except.lean

@@ -10,36 +10,39 @@ import Init.Control.Basic
 import Init.Control.Id
 import Init.Coe
 
-universes u v w u'
-
 namespace Except
 variable {ε : Type u}
 
-@[inline] protected def pure {α : Type v} (a : α) : Except ε α :=
+@[inline] protected def pure (a : α) : Except ε α :=
   Except.ok a
 
-@[inline] protected def map {α β : Type v} (f : α → β) : Except ε α → Except ε β
+@[inline] protected def map (f : α → β) : Except ε α → Except ε β
   | Except.error err => Except.error err
   | Except.ok v => Except.ok <| f v
 
-@[inline] protected def mapError {ε' : Type u} {α : Type v} (f : ε → ε') : Except ε α → Except ε' α
+@[simp] theorem map_id : Except.map (ε := ε) (α := α) (β := α) id = id := by
+  apply funext
+  intro e
+  simp [Except.map]; cases e <;> rfl
+
+@[inline] protected def mapError (f : ε → ε') : Except ε α → Except ε' α
   | Except.error err => Except.error <| f err
   | Except.ok v      => Except.ok v
 
-@[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
+@[inline] protected def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
   match ma with
   | Except.error err => Except.error err
   | Except.ok v      => f v
 
-@[inline] protected def toBool {α : Type v} : Except ε α → Bool
+@[inline] protected def toBool : Except ε α → Bool
   | Except.ok _    => true
   | Except.error _ => false
 
-@[inline] protected def toOption {α : Type v} : Except ε α → Option α
+@[inline] protected def toOption : Except ε α → Option α
   | Except.ok a    => some a
   | Except.error _ => none
 
-@[inline] protected def tryCatch {α : Type u} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
+@[inline] protected def tryCatch (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
   match ma with
   | Except.ok a    => Except.ok a
   | Except.error e => handle e

stage0/src/Init/Control/Lawful.lean

@@ -5,6 +5,8 @@ Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
+import Init.Control.Except
+import Init.Control.StateRef
 
 open Function
 
@@ -17,6 +19,9 @@ export LawfulFunctor (map_const id_map comp_map)
 
 attribute [simp] id_map
 
+@[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
+  id_map x
+
 class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where
   seqLeft_eq  (x : f α) (y : f β)     : x <* y = const β <$> x <*> y
   seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
@@ -24,6 +29,9 @@ class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFu
   map_pure    (g : α → β) (x : α)     : g <$> (pure x : f α) = pure (g x)
   seq_pure    (g : f (α → β)) (x : α) : g <*> pure x = (fun h : α → β => h x) <$> g
   seq_assoc   (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = (@comp α β γ <$> h) <*> g <*> x
+  comp_map g h x := by
+    repeat rw [← pure_seq]
+    simp [seq_assoc, map_pure, seq_pure]
 
 export LawfulApplicative (seqLeft_eq seqRight_eq pure_seq map_pure seq_pure seq_assoc)
 
@@ -37,6 +45,15 @@ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m
   bind_map       (f : m (α → (β : Type u))) (x : m α) : f >>= (. <$> x) = f <*> x
   pure_bind      (x : α) (f : α → m β) : pure x >>= f = f x
   bind_assoc     (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun x => f x >>= g
+  map_pure g x    := by rw [← bind_pure_comp, pure_bind]
+  seq_pure g x    := by rw [← bind_map]; simp [map_pure, bind_pure_comp]
+  seq_assoc x g h := by
+    -- TODO: support for applying `symm` at `simp` arguments
+    let bind_pure_comp_symm {α β : Type u} (f : α → β) (x : m α) : f <$> x = x >>= pure ∘ f := by
+      rw [bind_pure_comp]
+    let bind_map_symm {α β : Type u} (f : m (α → (β : Type u))) (x : m α) : f <*> x = f >>= (. <$> x) := by
+      rw [bind_map]
+    simp[bind_pure_comp_symm, bind_map_symm, bind_assoc, pure_bind]
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc
@@ -53,3 +70,208 @@ theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a
 
 theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
   simp [funext h]
+
+theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
+  rw [bind_map]
+
+theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
+  rw [seqRight_eq, ← bind_map, ← bind_pure_comp]
+  simp [Function.const]
+
+theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
+  rw [seqLeft_eq, ← bind_map, ← bind_pure_comp]
+  simp
+  apply bind_congr; intro
+  rw [← bind_pure_comp]
+
+/- Id -/
+
+namespace Id
+
+@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+
+instance : LawfulMonad Id := by
+  refine! { .. } <;> intros <;> rfl
+
+end Id
+
+/- ExceptT -/
+
+namespace ExceptT
+
+theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+  simp [run] at h
+  assumption
+
+@[simp] theorem run_pure [Monad m] : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
+@[simp] theorem run_lift [Monad m] : run (ExceptT.lift x : ExceptT ε m α) = Except.ok <$> x := rfl
+@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
+@[simp] theorem run_bind [Monad m] (x : ExceptT ε m α)
+        : run (x >>= f : ExceptT ε m β)
+          =
+          run x >>= fun
+                     | Except.ok x => run (f x)
+                     | Except.error e => pure (Except.error e) :=
+  rfl
+
+@[simp] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
+  simp [ExceptT.lift, pure, ExceptT.pure]
+
+@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
+    : (f <$> x).run = Except.map f <$> x.run := by
+  rw [← bind_pure_comp (m := m)]
+  simp [Functor.map, ExceptT.map]
+  apply bind_congr
+  intro a; cases a <;> simp [Except.map]
+
+protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
+  rfl
+
+protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
+  intros; rfl
+
+protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
+  show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
+  rw [← ExceptT.bind_pure_comp]
+  apply ext
+  simp
+  apply bind_congr
+  intro a
+  cases a with
+  | error => simp
+  | ok =>
+    simp; rw [← bind_pure_comp]; apply bind_congr; intro b;
+    cases b <;> simp [comp, Except.map, const]
+
+protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
+  show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
+  rw [← ExceptT.bind_pure_comp]
+  apply ext
+  simp
+  apply bind_congr
+  intro a; cases a <;> simp
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
+  id_map         := by intros; apply ext; simp
+  map_const      := by intros; rfl
+  seqLeft_eq     := ExceptT.seqLeft_eq
+  seqRight_eq    := ExceptT.seqRight_eq
+  pure_seq       := by intros; apply ext; simp [ExceptT.seq_eq]
+  bind_pure_comp := ExceptT.bind_pure_comp
+  bind_map       := by intros; rfl
+  pure_bind      := by intros; apply ext; simp
+  bind_assoc     := by intros; apply ext; simp; apply bind_congr; intro a; cases a <;> simp
+
+end ExceptT
+
+/- ReaderT -/
+
+namespace ReaderT
+
+theorem ext [Monad m] {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
+  simp [run] at h
+  exact funext h
+
+@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
+@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
+    : (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
+@[simp] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
+    : (f <$> x).run ctx = f <$> x.run ctx := rfl
+@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
+    : (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
+@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
+    : (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
+@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
+@[simp] theorem run_seq {α β : Type u} [Monad m] [LawfulMonad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ) : (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := by
+  rw [seq_eq_bind (m := m)]; rfl
+@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x *> y).run ctx = (x.run ctx *> y.run ctx) := by
+  rw [seqRight_eq_bind (m := m)]; rfl
+@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x <* y).run ctx = (x.run ctx <* y.run ctx) := by
+  rw [seqLeft_eq_bind (m := m)]; rfl
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
+  id_map         := by intros; apply ext; intros; simp
+  map_const      := by intros; rfl
+  seqLeft_eq     := by intros; apply ext; intros; simp; apply LawfulApplicative.seqLeft_eq
+  seqRight_eq    := by intros; apply ext; intros; simp; apply LawfulApplicative.seqRight_eq
+  pure_seq       := by intros; apply ext; intros; simp; apply LawfulApplicative.pure_seq
+  bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
+  bind_map       := by intros; rfl
+  pure_bind      := by intros; apply ext; intros; simp
+  bind_assoc     := by intros; apply ext; intros; simp
+
+end ReaderT
+
+/- StateRefT -/
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
+  inferInstanceAs (LawfulMonad (ReaderT (ST.Ref ω σ) m))
+
+/- StateT -/
+
+namespace StateT
+
+theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
+  funext h
+
+@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
+
+@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
+    : (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2 := by
+  simp [bind, StateT.bind, run]
+  apply bind_congr
+  intro p; cases p; rfl
+
+@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
+  simp [Functor.map, StateT.map, run]
+  rw [← bind_pure_comp]
+  apply bind_congr
+  intro p; cases p; rfl
+
+@[simp] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
+
+@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
+
+@[simp] theorem run_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
+
+@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ)
+    : (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
+
+@[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by
+  show (f >>= fun g => g <$> x).run s = _
+  simp
+
+@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
+  show (x >>= fun _ => y).run s = _
+  simp
+
+@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
+  show (x >>= fun a => y >>= fun _ => pure a).run s = _
+  simp
+
+theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
+  apply ext; intro s
+  simp; rw [← bind_pure_comp]; simp
+  apply bind_congr; intro p; cases p
+  simp[Prod.ext]
+
+theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
+  apply ext; intro s
+  simp; rw [← bind_pure_comp]; simp
+  apply bind_congr; intro p; cases p
+  simp[Prod.ext, const]; rw [← bind_pure_comp]
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
+  id_map         := by intros; apply ext; intros; simp[Prod.ext]
+  map_const      := by intros; rfl
+  seqLeft_eq     := seqLeft_eq
+  seqRight_eq    := seqRight_eq
+  pure_seq       := by intros; apply ext; intros; simp
+  bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
+  bind_map       := by intros; rfl
+  pure_bind      := by intros; apply ext; intros; simp
+  bind_assoc     := by intros; apply ext; intros; simp
+
+end StateT

stage0/src/Init/Core.lean

@@ -556,9 +556,6 @@ end
 
 /- Product -/
 
-section
-variable {α : Type u} {β : Type v}
-
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (arbitrary, arbitrary)
 
@@ -585,9 +582,11 @@ instance prodHasDecidableLt
 
 theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
   rfl
-end
 
-def Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
+theorem Prod.ext (p : α × β) : (p.1, p.2) = p := by
+  cases p; rfl
+
+def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 

stage0/src/Init/Prelude.lean

@@ -18,8 +18,8 @@ abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (
 abbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
   fun x => a
 
-@[reducible] def inferInstance {α : Type u} [i : α] : α := i
-@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i
+@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
+@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i
 
 set_option bootstrap.inductiveCheckResultingUniverse false in
 inductive PUnit : Sort u where
@@ -61,6 +61,8 @@ abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m :
 
 @[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
 
+@[simp] theorem id_eq (a : α) : Eq (id a) a := rfl
+
 theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b :=
   Eq.ndrec h₂ h₁
 
@@ -1183,12 +1185,12 @@ instance (m) : MonadLiftT m m where
     but not restricted to monad transformers.
     Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/
 class MonadFunctor (m : Type u → Type v) (n : Type u → Type w) where
-  monadMap {α : Type u} : (∀ {β}, m β → m β) → n α → n α
+  monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
 
 /-- The reflexive-transitive closure of `MonadFunctor`.
     `monadMap` is used to transitively lift Monad morphisms -/
 class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) where
-  monadMap {α : Type u} : (∀ {β}, m β → m β) → n α → n α
+  monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
 
 export MonadFunctorT (monadMap)
 
@@ -1302,7 +1304,7 @@ end ReaderT
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class MonadReader (ρ : outParam (Type u)) (n : Type u → Type u) where
-      lift {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α) → n α
+      lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α
     ```
     -/
 class MonadReaderOf (ρ : Type u) (m : Type u → Type v) where

stage0/src/Lean/Util/ReplaceExpr.lean

@@ -19,7 +19,7 @@ structure State where
 abbrev ReplaceM := StateM State
 
 @[inline] unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
-  modify fun s => { keys := s.keys.uset i key lcProof, results := s.results.uset i result lcProof };
+  modify fun ⟨keys, results⟩ => { keys := keys.uset i key lcProof, results := results.uset i result lcProof };
   pure result
 
 @[inline] unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) (e : Expr) : ReplaceM Expr := do

stage0/stdlib/Init/Control/Except.c

@@ -55,7 +55,6 @@ lean_object* l_instMonadExceptOfExceptT__1___rarg___lambda__1(lean_object*, lean
 lean_object* l_ExceptT_instMonadLiftExceptT(lean_object*, lean_object*);
 lean_object* l_ExceptT_bindCont___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_instMonadExceptT___rarg(lean_object*);
-lean_object* l_Except_tryCatch_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_map___rarg(lean_object*, lean_object*);
 lean_object* l_tryFinally(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_instMonadExceptT___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@@ -69,6 +68,7 @@ lean_object* l_Except_mapError___rarg(lean_object*, lean_object*);
 lean_object* l_Except_toBool(lean_object*, lean_object*);
 lean_object* l_ExceptT_instMonadFunctorExceptT(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_instMonadExcept___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ExceptT_bindCont_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_map(lean_object*, lean_object*, lean_object*);
 lean_object* l_instMonadExceptOfExceptT(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_instMonadExcept___closed__10;
@@ -116,7 +116,6 @@ lean_object* l_instMonadExceptOfExcept___lambda__1(lean_object*, lean_object*);
 lean_object* l_ExceptT_instMonadLiftExceptExceptT___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_bindCont___at_ExceptT_instMonadExceptT___spec__1(lean_object*, lean_object*);
 lean_object* l_ExceptT_tryCatch(lean_object*, lean_object*);
-lean_object* l_Except_tryCatch_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_finally_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_instMonadExcept___closed__5;
 lean_object* l_ExceptT_mk(lean_object*, lean_object*, lean_object*);
@@ -131,6 +130,7 @@ lean_object* l_ExceptT_bindCont___at_ExceptT_instMonadExceptT___spec__2(lean_obj
 lean_object* l_ExceptT_run___rarg___boxed(lean_object*);
 lean_object* l_Except_toOption(lean_object*, lean_object*);
 lean_object* l_MonadExcept_orelse_x27___rarg___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_ExceptT_bindCont_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_instMonadExcept___closed__9;
 lean_object* l_ExceptT_run___rarg(lean_object*);
 lean_object* l_Except_instMonadExcept___closed__1;
@@ -458,39 +458,6 @@ lean_dec(x_1);
 return x_2;
 }
 }
-lean_object* l_Except_tryCatch_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-lean_object* x_4; lean_object* x_5; 
-lean_dec(x_2);
-x_4 = lean_ctor_get(x_1, 0);
-lean_inc(x_4);
-lean_dec(x_1);
-x_5 = lean_apply_1(x_3, x_4);
-return x_5;
-}
-else
-{
-lean_object* x_6; lean_object* x_7; 
-lean_dec(x_3);
-x_6 = lean_ctor_get(x_1, 0);
-lean_inc(x_6);
-lean_dec(x_1);
-x_7 = lean_apply_1(x_2, x_6);
-return x_7;
-}
-}
-}
-lean_object* l_Except_tryCatch_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = lean_alloc_closure((void*)(l_Except_tryCatch_match__1___rarg), 3, 0);
-return x_4;
-}
-}
 lean_object* l_Except_tryCatch___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -949,6 +916,39 @@ x_3 = lean_alloc_closure((void*)(l_ExceptT_pure___rarg), 3, 0);
 return x_3;
 }
 }
+lean_object* l_ExceptT_bindCont_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_ExceptT_bindCont_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_ExceptT_bindCont_match__1___rarg), 3, 0);
+return x_4;
+}
+}
 lean_object* l_ExceptT_bindCont___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {

stage0/stdlib/Init/Control/Lawful.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Control.Lawful
-// Imports: Init.SimpLemmas
+// Imports: Init.SimpLemmas Init.Control.Except Init.Control.StateRef
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -13,7 +13,44 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* l_ExceptT_run__bind_match__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_ExceptT_run__bind_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_ExceptT_run__bind_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_ExceptT_run__bind_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_ExceptT_run__bind_match__1___rarg), 3, 0);
+return x_4;
+}
+}
 lean_object* initialize_Init_SimpLemmas(lean_object*);
+lean_object* initialize_Init_Control_Except(lean_object*);
+lean_object* initialize_Init_Control_StateRef(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Init_Control_Lawful(lean_object* w) {
 lean_object * res;
@@ -22,6 +59,12 @@ _G_initialized = true;
 res = initialize_Init_SimpLemmas(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Control_Except(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Control_StateRef(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Std/Control/Lawful.c

@@ -1,29 +0,0 @@
-// Lean compiler output
-// Module: Std.Control.Lawful
-// Imports: Init
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-lean_object* initialize_Init(lean_object*);
-static bool _G_initialized = false;
-lean_object* initialize_Std_Control_Lawful(lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Init(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif