chore: update stage0

stage0/src/Init/Control/Except.lean

@@ -59,11 +59,10 @@ variables {ε : Type u}
   | Except.ok a    => Except.ok a
   | Except.error e => handle e
 
-instance : Monad (Except ε) := {
+instance : Monad (Except ε) where
   pure := Except.pure
   bind := Except.bind
   map  := Except.map
-}
 
 end Except
 
@@ -105,31 +104,27 @@ instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
 
 instance : MonadFunctor m (ExceptT ε m) := ⟨fun f x => f x⟩
 
-instance : Monad (ExceptT ε m) := {
+instance : Monad (ExceptT ε m) where
   pure := ExceptT.pure
   bind := ExceptT.bind
   map  := ExceptT.map
-}
 
 @[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
   ExceptT.mk <| Except.mapError f <$> x
 
 end ExceptT
 
-instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) := {
-  throw    := fun e        => ExceptT.mk <| throwThe ε₁ e
-  tryCatch := fun x handle => ExceptT.mk <| tryCatchThe ε₁ x handle
-}
+instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
+  throw e := ExceptT.mk <| throwThe ε₁ e
+  tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 
-instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) := {
-  throw    := fun e => ExceptT.mk <| pure (Except.error e)
+instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where
+  throw e := ExceptT.mk <| pure (Except.error e)
   tryCatch := ExceptT.tryCatch
-}
 
-instance (ε) : MonadExceptOf ε (Except ε) := {
+instance (ε) : MonadExceptOf ε (Except ε) where
   throw    := Except.error
   tryCatch := Except.tryCatch
-}
 
 namespace MonadExcept
 variables {ε : Type u} {m : Type v → Type w}
@@ -144,11 +139,10 @@ end MonadExcept
 @[inline] def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
   tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
 
-instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) := {
-  stM      := Except ε
-  liftWith := fun f => liftM <| f fun x => x.run
-  restoreM := fun x => x
-}
+instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) where
+  stM        := Except ε
+  liftWith f := liftM <| f fun x => x.run
+  restoreM x := x
 
 class MonadFinally (m : Type u → Type v) :=
   (tryFinally' {α β} : m α → (Option α → m β) → m (α × β))
@@ -160,14 +154,13 @@ export MonadFinally (tryFinally')
   let y := tryFinally' x (fun _ => finalizer)
   (·.1) <$> y
 
-instance Id.finally : MonadFinally Id := {
+instance Id.finally : MonadFinally Id where
   tryFinally' := fun x h =>
    let a := x
    let b := h (some x)
    pure (a, b)
-}
 
-instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) := {
+instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) where
   tryFinally' := fun x h => ExceptT.mk do
     let r ← tryFinally' x fun e? => match e? with
         | some (Except.ok a) => h (some a)
@@ -176,4 +169,3 @@ instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m]
     | (Except.ok a,    Except.ok b)    => pure (Except.ok (a, b))
     | (_,              Except.error e) => pure (Except.error e)  -- second error has precedence
     | (Except.error e, _)              => pure (Except.error e)
-}

stage0/src/Init/Control/State.lean

@@ -45,11 +45,10 @@ variables [Monad m] {α β : Type u}
 @[inline] protected def map (f : α → β) (x : StateT σ m α) : StateT σ m β :=
   fun s => do let (a, s) ← x s; pure (f a, s)
 
-instance : Monad (StateT σ m) := {
+instance : Monad (StateT σ m) where
   pure := StateT.pure
   bind := StateT.bind
   map  := StateT.map
-}
 
 @[inline] protected def orElse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
   fun s => x₁ s <|> x₂ s
@@ -57,10 +56,9 @@ instance : Monad (StateT σ m) := {
 @[inline] protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
   fun s => failure
 
-instance [Alternative m] : Alternative (StateT σ m) := {
-  failure := StateT.failure,
+instance [Alternative m] : Alternative (StateT σ m) where
+  failure := StateT.failure
   orElse  := StateT.orElse
-}
 
 @[inline] protected def get : StateT σ m σ :=
   fun s => pure (s, s)
@@ -89,24 +87,21 @@ end StateT
 section
 variables {σ : Type u} {m : Type u → Type v}
 
-instance [Monad m] : MonadStateOf σ (StateT σ m) := {
+instance [Monad m] : MonadStateOf σ (StateT σ m) where
   get       := StateT.get
   set       := StateT.set
   modifyGet := StateT.modifyGet
-}
 
 end
 
-instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) := {
+instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) where
   stM      := fun α   => α × σ
   liftWith := fun f => do let s ← get; liftM (f (fun x => x.run s))
   restoreM := fun x => do let (a, s) ← liftM x; set s; pure a
-}
 
-instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) := {
+instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) where
   tryFinally' := fun x h s => do
     let ((a, _), (b, s'')) ← tryFinally' (x s) fun
       | some (a, s') => h (some a) s'
       | none         => h none s
     pure ((a, b), s'')
-}

stage0/src/Init/Core.lean

@@ -432,29 +432,23 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
 
 /- Inhabited -/
 
-instance : Inhabited Prop := {
+instance : Inhabited Prop where
   default := True
-}
 
-instance : Inhabited Bool := {
+instance : Inhabited Bool where
   default := false
-}
 
-instance : Inhabited True := {
+instance : Inhabited True where
   default := trivial
-}
 
-instance : Inhabited NonScalar := {
+instance : Inhabited NonScalar where
   default := ⟨arbitrary _⟩
-}
 
-instance : Inhabited PNonScalar.{u} := {
+instance : Inhabited PNonScalar.{u} where
   default := ⟨arbitrary _⟩
-}
 
-instance {α} [Inhabited α] : Inhabited (ForInStep α) := {
-  default:= ForInStep.done (arbitrary _)
-}
+instance {α} [Inhabited α] : Inhabited (ForInStep α) where
+  default := ForInStep.done (arbitrary _)
 
 class inductive Nonempty (α : Sort u) : Prop :=
   | intro (val : α) : Nonempty α
@@ -462,9 +456,8 @@ class inductive Nonempty (α : Sort u) : Prop :=
 protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
   h₂ h₁.1
 
-instance {α : Sort u} [Inhabited α] : Nonempty α := {
+instance {α : Sort u} [Inhabited α] : Nonempty α where
   val := arbitrary α
-}
 
 theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
   | ⟨w, h⟩ => ⟨w⟩
@@ -539,9 +532,8 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
   exact rfl
 
-instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} := {
+instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
   default := ⟨a, h⟩
-}
 
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
@@ -555,13 +547,11 @@ end Subtype
 section
 variables {α : Type u} {β : Type v}
 
-instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) := {
+instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) where
   default := Sum.inl (arbitrary α)
-}
 
-instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) := {
+instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) where
   default := Sum.inr (arbitrary β)
-}
 
 instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
   match a, b with
@@ -581,9 +571,8 @@ end
 section
 variables {α : Type u} {β : Type v}
 
-instance [Inhabited α] [Inhabited β] : Inhabited (α × β) := {
+instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (arbitrary α, arbitrary β)
-}
 
 instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
   fun ⟨a, b⟩ ⟨a', b'⟩ =>
@@ -594,13 +583,11 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
       | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
     | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))
 
-instance [BEq α] [BEq β] : BEq (α × β) := {
+instance [BEq α] [BEq β] : BEq (α × β) where
   beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂
-}
 
-instance [HasLess α] [HasLess β] : HasLess (α × β) := {
-  Less := fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
-}
+instance [HasLess α] [HasLess β] : HasLess (α × β) where
+  Less s t := s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
 
 instance prodHasDecidableLt
     [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β]
@@ -638,9 +625,8 @@ theorem punitEqPUnit (a : PUnit) : a = () :=
 instance : Subsingleton PUnit :=
   Subsingleton.intro punitEq
 
-instance : Inhabited PUnit := {
+instance : Inhabited PUnit where
   default := ⟨⟩
-}
 
 instance : DecidableEq PUnit :=
   fun a b => isTrue (punitEq a b)

stage0/src/Init/Prelude.lean

@@ -186,17 +186,14 @@ class Inhabited (α : Sort u) :=
 constant arbitrary (α : Sort u) [s : Inhabited α] : α :=
   @Inhabited.default α s
 
-instance : Inhabited (Sort u) := {
+instance : Inhabited (Sort u) where
   default := PUnit
-}
 
-instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {
+instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => arbitrary β
-}
 
-instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {
+instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
   default := fun a => arbitrary (β a)
-}
 
 /-- Universe lifting operation from Sort to Type -/
 structure PLift (α : Sort u) : Type u :=
@@ -214,9 +211,8 @@ structure PointedType :=
   (type : Type u)
   (val : type)
 
-instance : Inhabited PointedType.{u} := {
+instance : Inhabited PointedType.{u} where
   default := { type := PUnit.{u+1}, val := ⟨⟩ }
-}
 
 /-- Universe lifting operation -/
 structure ULift.{r, s} (α : Type s) : Type (max s r) :=
@@ -279,8 +275,8 @@ class BEq      (α : Type u) := (beq : α → α → Bool)
 
 open BEq (beq)
 
-instance {α : Type u} [DecidableEq α] : BEq α :=
-  ⟨fun a b => decide (Eq a b)⟩
+instance {α : Type u} [DecidableEq α] : BEq α where
+  beq a b := decide (Eq a b)
 
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
@@ -346,11 +342,11 @@ class OfNat (α : Type u) :=
 export OfNat (ofNat)
 
 @[defaultInstance]
-instance : OfNat Nat := ⟨id⟩
+instance : OfNat Nat where
+  ofNat x := x
 
-instance : Inhabited Nat := {
+instance : Inhabited Nat where
   default := 0
-}
 
 class HasLessEq (α : Type u) := (LessEq : α → α → Prop)
 class HasLess   (α : Type u) := (Less : α → α → Prop)
@@ -384,9 +380,8 @@ protected def Nat.add : (@& Nat) → (@& Nat) → Nat
   | a, Nat.zero   => a
   | a, Nat.succ b => Nat.succ (Nat.add a b)
 
-instance : Add Nat := {
+instance : Add Nat where
   add := Nat.add
-}
 
 /- We mark the following definitions as pattern to make sure they can be used in recursive equations,
    and reduced by the equation Compiler. -/
@@ -398,9 +393,8 @@ protected def Nat.mul : (@& Nat) → (@& Nat) → Nat
   | a, 0          => 0
   | a, Nat.succ b => Nat.add (Nat.mul a b) a
 
-instance : Mul Nat := {
+instance : Mul Nat where
   mul := Nat.mul
-}
 
 set_option bootstrap.gen_matcher_code false in
 @[extern "lean_nat_pow"]
@@ -408,9 +402,8 @@ protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat
   | 0      => 1
   | succ n => Nat.mul (Nat.pow m n) m
 
-instance : Pow Nat Nat := {
+instance : Pow Nat Nat where
   pow := Nat.pow
-}
 
 set_option bootstrap.gen_matcher_code false in
 @[extern "lean_nat_dec_eq"]
@@ -567,9 +560,8 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
   | a, 0      => a
   | a, succ b => pred (Nat.sub a b)
 
-instance : Sub Nat := {
+instance : Sub Nat where
   sub := Nat.sub
-}
 
 theorem Nat.predLePred : {n m : Nat} → LessEq n m → LessEq (pred n) (pred m)
   | zero,   zero,   h => rfl
@@ -641,9 +633,8 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
 
 instance : DecidableEq UInt8 := UInt8.decEq
 
-instance : Inhabited UInt8 := {
+instance : Inhabited UInt8 where
   default := UInt8.ofNatCore 0 decide!
-}
 
 def UInt16.size : Nat := 65536
 structure UInt16 :=
@@ -666,9 +657,8 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
 
 instance : DecidableEq UInt16 := UInt16.decEq
 
-instance : Inhabited UInt16 := {
+instance : Inhabited UInt16 where
   default := UInt16.ofNatCore 0 decide!
-}
 
 def UInt32.size : Nat := 4294967296
 structure UInt32 :=
@@ -694,9 +684,8 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
 
 instance : DecidableEq UInt32 := UInt32.decEq
 
-instance : Inhabited UInt32 := {
+instance : Inhabited UInt32 where
   default := UInt32.ofNatCore 0 decide!
-}
 
 def UInt32.lt (a b : UInt32) : Prop := Less a.val b.val
 def UInt32.le (a b : UInt32) : Prop := LessEq a.val b.val
@@ -740,9 +729,8 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
 
 instance : DecidableEq UInt64 := UInt64.decEq
 
-instance : Inhabited UInt64 := {
+instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 decide!
-}
 
 def USize.size : Nat := pow 2 System.Platform.numBits
 
@@ -772,9 +760,10 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
 
 instance : DecidableEq USize := USize.decEq
 
-instance : Inhabited USize := {
-  default := USize.ofNatCore 0 (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!)
-}
+instance : Inhabited USize where
+  default := USize.ofNatCore 0 (match USize.size, usizeSzEq with
+    | _, Or.inl rfl => decide!
+    | _, Or.inr rfl => decide!)
 
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : Less n 4294967296) : USize := {
@@ -849,17 +838,15 @@ attribute [unbox] Option
 
 export Option (none some)
 
-instance {α} : Inhabited (Option α) := {
+instance {α} : Inhabited (Option α) where
   default := none
-}
 
 inductive List (α : Type u) :=
   | nil : List α
   | cons (head : α) (tail : List α) : List α
 
-instance {α} : Inhabited (List α) := {
+instance {α} : Inhabited (List α) where
   default := List.nil
-}
 
 protected def List.hasDecEq {α: Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
   | nil,       nil       => isTrue rfl
@@ -1064,13 +1051,11 @@ export MonadLiftT (monadLift)
 
 abbrev liftM := @monadLift
 
-instance (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o := {
-  monadLift := fun x => MonadLift.monadLift (m := n) (monadLift x)
-}
+instance (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o where
+  monadLift x := MonadLift.monadLift (m := n) (monadLift x)
 
-instance (m) : MonadLiftT m m := {
-  monadLift := fun x => x
-}
+instance (m) : MonadLiftT m m where
+  monadLift x := x
 
 /-- A functor in the category of monads. Can be used to lift monad-transforming functions.
     Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),
@@ -1086,13 +1071,11 @@ class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) :=
 
 export MonadFunctorT (monadMap)
 
-instance (m n o) [MonadFunctorT m n] [MonadFunctor n o] : MonadFunctorT m o := {
-  monadMap := fun f => MonadFunctor.monadMap (m := n) (monadMap (m := m) f)
-}
+instance (m n o) [MonadFunctorT m n] [MonadFunctor n o] : MonadFunctorT m o where
+  monadMap f := MonadFunctor.monadMap (m := n) (monadMap (m := m) f)
 
-instance monadFunctorRefl (m) : MonadFunctorT m m := {
-  monadMap := fun f => f
-}
+instance monadFunctorRefl (m) : MonadFunctorT m m where
+  monadMap f := f
 
 inductive Except (ε : Type u) (α : Type v) :=
   | error : ε → Except ε α
@@ -1121,10 +1104,9 @@ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
 
 export MonadExcept (throw tryCatch)
 
-instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m := {
+instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
   throw    := throwThe ε
   tryCatch := tryCatchThe ε
-}
 
 namespace MonadExcept
 variables {ε : Type u} {m : Type v → Type w}
@@ -1158,10 +1140,9 @@ variables {ρ : Type u} {m : Type u → Type v} {α : Type u}
 
 instance  : MonadLift m (ReaderT ρ m) := ⟨ReaderT.lift⟩
 
-instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) := {
+instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) where
   throw    := Function.comp ReaderT.lift (throwThe ε)
   tryCatch := fun x c r => tryCatchThe ε (x r) (fun e => (c e) r)
-}
 
 end
 
@@ -1180,11 +1161,10 @@ variables {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}
 @[inline] protected def map (f : α → β) (x : ReaderT ρ m α) : ReaderT ρ m β :=
   fun r => Functor.map f (x r)
 
-instance : Monad (ReaderT ρ m) := {
+instance : Monad (ReaderT ρ m) where
   pure := ReaderT.pure
   bind := ReaderT.bind
   map  := ReaderT.map
-}
 
 instance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) := ⟨fun f x r => f (x r)⟩
 
@@ -1277,11 +1257,10 @@ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :=
 
 export MonadState (get modifyGet)
 
-instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m := {
+instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m where
   set       := MonadStateOf.set
   get       := getThe σ
   modifyGet := fun f => MonadStateOf.modifyGet f
-}
 
 @[inline] def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m PUnit :=
   modifyGet fun s => (PUnit.unit, f s)
@@ -1291,11 +1270,10 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
 -- will be picked first
-instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n := {
+instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n where
   get       := liftM (m := m) MonadStateOf.get
   set       := fun s => liftM (m := m) (MonadStateOf.set s)
   modifyGet := fun f => monadLift (m := m) (MonadState.modifyGet f)
-}
 
 namespace EStateM
 
@@ -1372,27 +1350,23 @@ class Backtrackable (δ : outParam (Type u)) (σ : Type u) :=
   | Result.ok _ s    => y s
   | Result.error e s => Result.error e s
 
-instance : Monad (EStateM ε σ) := {
+instance : Monad (EStateM ε σ) where
   bind     := EStateM.bind
   pure     := EStateM.pure
   map      := EStateM.map
   seqRight := EStateM.seqRight
-}
 
-instance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) := {
+instance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) where
   orElse := EStateM.orElse
-}
 
-instance : MonadStateOf σ (EStateM ε σ) := {
+instance : MonadStateOf σ (EStateM ε σ) where
   set       := EStateM.set
   get       := EStateM.get
   modifyGet := EStateM.modifyGet
-}
 
-instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) := {
+instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where
   throw    := EStateM.throw
   tryCatch := EStateM.tryCatch
-}
 
 @[inline] def run (x : EStateM ε σ α) (s : σ) : Result ε σ α :=
   x s
@@ -1407,10 +1381,9 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) := {
 @[inline] def dummyRestore : σ → PUnit → σ := fun s _ => s
 
 /- Dummy default instance -/
-instance nonBacktrackable : Backtrackable PUnit σ := {
+instance nonBacktrackable : Backtrackable PUnit σ where
   save    := dummySave
   restore := dummyRestore
-}
 
 end EStateM
 
@@ -1624,11 +1597,10 @@ class MonadQuotation (m : Type → Type) :=
 
 export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
-instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m n] : MonadQuotation n := {
+instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m n] : MonadQuotation n where
   getCurrMacroScope   := liftM (m := m) getCurrMacroScope
   getMainModule       := liftM (m := m) getMainModule
   withFreshMacroScope := monadMap (m := m) withFreshMacroScope
-}
 
 /-
 We represent a name with macro scopes as
@@ -1762,10 +1734,9 @@ class MonadRef (m : Type → Type) :=
 
 export MonadRef (getRef)
 
-instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n := {
+instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n where
   getRef  := liftM (getRef : m _)
   withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x
-}
 
 def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
   match ref.getPos with
@@ -1805,10 +1776,9 @@ abbrev Macro := Syntax → MacroM Syntax
 
 namespace Macro
 
-instance : MonadRef MacroM := {
+instance : MonadRef MacroM where
   getRef     := bind read fun ctx => pure ctx.ref
   withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
-}
 
 def addMacroScope (n : Name) : MacroM Name :=
   bind read fun ctx =>
@@ -1834,11 +1804,10 @@ def throwErrorAt {α} (ref : Syntax) (msg : String) : MacroM α :=
   | true  => throw (Exception.error ref maxRecDepthErrorMessage)
   | false => withReader (fun ctx => { ctx with currRecDepth := add ctx.currRecDepth 1 }) x
 
-instance : MonadQuotation MacroM := {
+instance : MonadQuotation MacroM where
   getCurrMacroScope   := fun ctx => pure ctx.currMacroScope
   getMainModule       := fun ctx => pure ctx.mainModule
   withFreshMacroScope := Macro.withFreshMacroScope
-}
 
 unsafe def mkMacroEnvImp (expandMacro? : Syntax → MacroM (Option Syntax)) : MacroEnv :=
   unsafeCast expandMacro?

stage0/src/Init/System/IO.lean

@@ -83,6 +83,11 @@ def ofExcept [ToString ε] (e : Except ε α) : IO α :=
 def lazyPure (fn : Unit → α) : IO α :=
   pure (fn ())
 
+
+def sleep (ms : UInt32) : IO Unit :=
+  -- TODO: add a proper primitive for IO.sleep
+  fun s => dbgSleep ms fun _ => EStateM.Result.ok () s
+
 /--
   Run `act` in a separate `Task`. This is similar to Haskell's [`unsafeInterleaveIO`](http://hackage.haskell.org/package/base-4.14.0.0/docs/System-IO-Unsafe.html#v:unsafeInterleaveIO),
   except that the `Task` is started eagerly as usual. Thus pure accesses to the `Task` do not influence the impure `act`

stage0/src/Lean.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Data
 import Lean.Compiler
 import Lean.Environment
 import Lean.Modifiers
@@ -25,3 +26,4 @@ import Lean.Delaborator
 import Lean.PrettyPrinter
 import Lean.CoreM
 import Lean.InternalExceptionId
+import Lean.Server

stage0/src/Lean/Data.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+import Lean.Data.Format
+import Lean.Data.FormatMacro
+import Lean.Data.Json
+import Lean.Data.JsonRpc
+import Lean.Data.KVMap
+import Lean.Data.LBool
+import Lean.Data.LOption
+import Lean.Data.Lsp
+import Lean.Data.Name
+import Lean.Data.Occurrences
+import Lean.Data.OpenDecl
+import Lean.Data.Options
+import Lean.Data.Position
+import Lean.Data.SMap
+import Lean.Data.Trie

stage0/src/Lean/Delaborator.lean

@@ -457,13 +457,20 @@ def delabMData : Delab := do
   -- only interpret `pp.` values by default
   let Expr.mdata m _ _ ← getExpr | unreachable!
   let mut posOpts := (← read).optionsPerPos
+  let mut inaccessible := false
   let pos := (← read).pos
   for (k, v) in m do
     if (`pp).isPrefixOf k then
       let opts := posOpts.find? pos |>.getD {}
       posOpts := posOpts.insert pos (opts.insert k v)
-  withReader ({ · with optionsPerPos := posOpts }) <|
-    withMDataExpr delab
+    if k == `inaccessible then
+      inaccessible := true
+  withReader ({ · with optionsPerPos := posOpts }) do
+    let s ← withMDataExpr delab
+    if inaccessible then
+      `(.($s))
+    else
+      pure s
 
 /--
 Check for a `Syntax.ident` of the given name anywhere in the tree.
@@ -780,6 +787,14 @@ def delabListToArray : Delab := whenPPOption getPPNotation do
   | `([$xs*]) => `(#[$xs*])
   | _         => failure
 
+@[builtinDelab app.namedPattern]
+def delabNamedPattern : Delab := do
+  guard $ (← getExpr).getAppNumArgs == 3
+  let x ← withAppFn $ withAppArg delab
+  let p ← withAppArg delab
+  guard x.isIdent
+  `($x:ident@$p:term)
+
 end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/

stage0/src/Lean/Elab/Match.lean

@@ -35,9 +35,9 @@ structure MatchAltView :=
   (rhs      : Syntax)
 
 def mkMatchAltView (ref : Syntax) (matchAlt : Syntax) : MatchAltView := {
-  ref := ref,
-  patterns := matchAlt[0].getSepArgs,
-  rhs := matchAlt[2]
+  ref      := ref
+  patterns := matchAlt[0].getSepArgs
+  rhs      := matchAlt[2]
 }
 
 private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do

stage0/src/Lean/Elab/Structure.lean

@@ -135,15 +135,20 @@ def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
 
 /-
 ```
-def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
-def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
-def structInstBinder     := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
+def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
+def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
+def structInstBinder     := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
+def structSimpleBinder   := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 ```
 -/
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
   let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
+    let mut fieldBinder := fieldBinder
+    if fieldBinder.getKind == `Lean.Parser.Command.structSimpleBinder then
+      fieldBinder := Syntax.node `Lean.Parser.Command.structExplicitBinder
+        #[ fieldBinder[0], mkAtomFrom fieldBinder "(", fieldBinder[1], fieldBinder[2], fieldBinder[3], fieldBinder[4], mkAtomFrom fieldBinder ")" ]
     let k := fieldBinder.getKind
     let binfo ←
       if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
@@ -178,12 +183,12 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
         throwError! "invalid field name '{name}', identifiers starting with '_' are reserved to the system"
       let declName := structDeclName ++ name
       let declName ← applyVisibility fieldModifiers.visibility declName
-      pure $ views.push {
+      return views.push {
         ref        := ident,
         modifiers  := fieldModifiers,
         binderInfo := binfo,
         inferMod   := inferMod,
-         declName   := declName,
+        declName   := declName,
         name       := name,
         binders    := binders,
         type?      := type?,

stage0/src/Lean/Elab/Tactic/Induction.lean

@@ -240,7 +240,10 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[1].getSepArgs
+  if inductionAlts.getNumArgs == 2 then
+    inductionAlts[1].getSepArgs -- TODO remove
+  else
+    inductionAlts[2].getSepArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]

stage0/src/Lean/Meta/Match/Basic.lean

@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Match.MatcherInfo
+import Lean.Meta.Match.CaseArraySizes
+
+namespace Lean.Meta.Match
+
+inductive Pattern : Type :=
+  | inaccessible (e : Expr) : Pattern
+  | var          (fvarId : FVarId) : Pattern
+  | ctor         (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern) : Pattern
+  | val          (e : Expr) : Pattern
+  | arrayLit     (type : Expr) (xs : List Pattern) : Pattern
+  | as           (varId : FVarId) (p : Pattern) : Pattern
+
+namespace Pattern
+
+instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩
+
+partial def toMessageData : Pattern → MessageData
+  | inaccessible e         => m!".({e})"
+  | var varId              => mkFVar varId
+  | ctor ctorName _ _ []   => ctorName
+  | ctor ctorName _ _ pats => m!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
+  | val e                  => e
+  | arrayLit _ pats        => m!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
+  | as varId p             => m!"{mkFVar varId}@{toMessageData p}"
+
+partial def toExpr (p : Pattern) (annotate := false) : MetaM Expr :=
+  visit p
+where
+  visit (p : Pattern) := do
+    match p with
+    | inaccessible e                 =>
+      if annotate then
+        pure (mkAnnotation `inaccessible e)
+      else
+        pure e
+    | var fvarId                     => pure $ mkFVar fvarId
+    | val e                          => pure e
+    | as fvarId p                    =>
+      if annotate then
+        mkAppM `namedPattern #[mkFVar fvarId, (← visit p)]
+      else
+        visit p
+    | arrayLit type xs               =>
+      let xs ← xs.mapM visit
+      mkArrayLit type xs
+    | ctor ctorName us params fields =>
+      let fields ← fields.mapM visit
+      pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
+
+/- Apply the free variable substitution `s` to the given pattern -/
+partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern
+  | inaccessible e  => inaccessible $ s.apply e
+  | ctor n us ps fs => ctor n us (ps.map s.apply) $ fs.map (applyFVarSubst s)
+  | val e           => val $ s.apply e
+  | arrayLit t xs   => arrayLit (s.apply t) $ xs.map (applyFVarSubst s)
+  | var fvarId      => match s.find? fvarId with
+    | some e => inaccessible e
+    | none   => var fvarId
+  | as fvarId p     => match s.find? fvarId with
+    | none   => as fvarId $ applyFVarSubst s p
+    | some _ => applyFVarSubst s p
+
+def replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern :=
+  let s : FVarSubst := {}
+  p.applyFVarSubst (s.insert fvarId v)
+
+partial def hasExprMVar : Pattern → Bool
+  | inaccessible e => e.hasExprMVar
+  | ctor _ _ ps fs => ps.any (·.hasExprMVar) || fs.any hasExprMVar
+  | val e          => e.hasExprMVar
+  | as _ p         => hasExprMVar p
+  | arrayLit t xs  => t.hasExprMVar || xs.any hasExprMVar
+  | _              => false
+
+end Pattern
+
+partial def instantiatePatternMVars : Pattern → MetaM Pattern
+  | Pattern.inaccessible e      => return Pattern.inaccessible (← instantiateMVars e)
+  | Pattern.val e               => return Pattern.val (← instantiateMVars e)
+  | Pattern.ctor n us ps fields => return Pattern.ctor n us (← ps.mapM instantiateMVars) (← fields.mapM instantiatePatternMVars)
+  | Pattern.as x p              => return Pattern.as x (← instantiatePatternMVars p)
+  | Pattern.arrayLit t xs       => return Pattern.arrayLit (← instantiateMVars t) (← xs.mapM instantiatePatternMVars)
+  | p                   => return p
+
+structure AltLHS :=
+  (ref        : Syntax)
+  (fvarDecls  : List LocalDecl) -- Free variables used in the patterns.
+  (patterns   : List Pattern)   -- We use `List Pattern` since we have nary match-expressions.
+
+def instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS :=
+  return { altLHS with
+    fvarDecls := (← altLHS.fvarDecls.mapM instantiateLocalDeclMVars),
+    patterns  := (← altLHS.patterns.mapM instantiatePatternMVars)
+  }
+
+structure Alt :=
+  (ref       : Syntax)
+  (idx       : Nat) -- for generating error messages
+  (rhs       : Expr)
+  (fvarDecls : List LocalDecl)
+  (patterns  : List Pattern)
+
+namespace Alt
+
+instance : Inhabited Alt := ⟨⟨arbitrary _, 0, arbitrary _, [], []⟩⟩
+
+partial def toMessageData (alt : Alt) : MetaM MessageData := do
+  withExistingLocalDecls alt.fvarDecls do
+    let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")"
+    let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs
+    addMessageContext msg
+
+def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
+  { alt with
+    patterns  := alt.patterns.map fun p => p.applyFVarSubst s,
+    fvarDecls := alt.fvarDecls.map fun d => d.applyFVarSubst s,
+    rhs       := alt.rhs.applyFVarSubst s }
+
+def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
+  { alt with
+    patterns  := alt.patterns.map fun p => p.replaceFVarId fvarId v,
+    fvarDecls :=
+      let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId
+      decls.map $ replaceFVarIdAtLocalDecl fvarId v,
+    rhs       := alt.rhs.replaceFVarId fvarId v }
+
+/-
+  Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`.
+  This extra check is necessary when performing dependent elimination and inaccessible terms have been used.
+  For example, consider the following code fragment:
+
+```
+inductive Vec (α : Type u) : Nat → Type u :=
+  | nil : Vec α 0
+  | cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
+
+inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop :=
+  | nil   : VecPred P Vec.nil
+  | cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
+
+theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
+  | _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
+```
+Recall that `_` in a pattern can be elaborated into pattern variable or an inaccessible term.
+The elaborator uses an inaccessible term when typing constraints restrict its value.
+Thus, in the example above, the `_` at `Vec.cons head _` becomes the inaccessible pattern `.(Vec.nil)`
+because the type ascription `(w : VecPred P Vec.nil)` propagates typing constraints that restrict its value to be `Vec.nil`.
+After elaboration the alternative becomes:
+```
+  | .(0), @Vec.cons .(α) .(0) head .(Vec.nil), @VecPred.cons .(α) .(P) .(0) .(head) .(Vec.nil) h w => ⟨head, h⟩
+```
+where
+```
+(head : α), (h: P head), (w : VecPred P Vec.nil)
+```
+Then, when we process this alternative in this module, the following check will detect that
+`w` has type `VecPred P Vec.nil`, when it is supposed to have type `VecPred P tail`.
+Note that if we had written
+```
+theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
+  | _, Vec.cons head Vec.nil, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
+```
+we would get the easier to digest error message
+```
+missing cases:
+_, (Vec.cons _ _ (Vec.cons _ _ _)), _
+```
+-/
+def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt := do
+  match alt.fvarDecls.find? fun (fvarDecl : LocalDecl) => fvarDecl.fvarId == fvarId with
+  | none          => throwErrorAt alt.ref "unknown free pattern variable"
+  | some fvarDecl => do
+    let vType ← inferType v
+    unless (← isDefEqGuarded fvarDecl.type vType) do
+      withExistingLocalDecls alt.fvarDecls do
+        throwErrorAt alt.ref $
+          m!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
+    pure $ replaceFVarId fvarId v alt
+
+end Alt
+
+inductive Example :=
+  | var        : FVarId → Example
+  | underscore : Example
+  | ctor       : Name → List Example → Example
+  | val        : Expr → Example
+  | arrayLit   : List Example → Example
+
+namespace Example
+
+partial def replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example
+  | var x        => if x == fvarId then ex else var x
+  | ctor n exs   => ctor n $ exs.map (replaceFVarId fvarId ex)
+  | arrayLit exs => arrayLit $ exs.map (replaceFVarId fvarId ex)
+  | ex           => ex
+
+partial def applyFVarSubst (s : FVarSubst) : Example → Example
+  | var fvarId =>
+    match s.get fvarId with
+    | Expr.fvar fvarId' _ => var fvarId'
+    | _                   => underscore
+  | ctor n exs   => ctor n $ exs.map (applyFVarSubst s)
+  | arrayLit exs => arrayLit $ exs.map (applyFVarSubst s)
+  | ex           => ex
+
+partial def varsToUnderscore : Example → Example
+  | var x        => underscore
+  | ctor n exs   => ctor n $ exs.map varsToUnderscore
+  | arrayLit exs => arrayLit $ exs.map varsToUnderscore
+  | ex           => ex
+
+partial def toMessageData : Example → MessageData
+  | var fvarId        => mkFVar fvarId
+  | ctor ctorName []  => mkConst ctorName
+  | ctor ctorName exs => "(" ++ mkConst ctorName ++ exs.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")"
+  | arrayLit exs      => "#" ++ MessageData.ofList (exs.map toMessageData)
+  | val e             => e
+  | underscore        => "_"
+
+end Example
+
+def examplesToMessageData (cex : List Example) : MessageData :=
+  MessageData.joinSep (cex.map (Example.toMessageData ∘ Example.varsToUnderscore)) ", "
+
+structure Problem :=
+  (mvarId        : MVarId)
+  (vars          : List Expr)
+  (alts          : List Alt)
+  (examples      : List Example)
+
+def withGoalOf {α} (p : Problem) (x : MetaM α) : MetaM α :=
+  withMVarContext p.mvarId x
+
+instance : Inhabited Problem := ⟨{ mvarId := arbitrary _, vars := [], alts := [], examples := []}⟩
+
+def Problem.toMessageData (p : Problem) : MetaM MessageData :=
+  withGoalOf p do
+    let alts ← p.alts.mapM Alt.toMessageData
+    let vars ← p.vars.mapM fun x => do let xType ← inferType x; pure (x ++ ":(" ++ xType ++ ")" : MessageData)
+    return "remaining variables: " ++ vars
+      ++ Format.line ++ "alternatives:" ++ indentD (MessageData.joinSep alts Format.line)
+      ++ Format.line ++ "examples: " ++ examplesToMessageData p.examples
+      ++ Format.line
+
+abbrev CounterExample := List Example
+
+def counterExampleToMessageData (cex : CounterExample) : MessageData :=
+  examplesToMessageData cex
+
+def counterExamplesToMessageData (cexs : List CounterExample) : MessageData :=
+  MessageData.joinSep (cexs.map counterExampleToMessageData) Format.line
+
+structure MatcherResult :=
+  (matcher         : Expr) -- The matcher. It is not just `Expr.const matcherName` because the type of the major premises may contain free variables.
+  (counterExamples : List CounterExample)
+  (unusedAltIdxs   : List Nat)
+
+end Lean.Meta.Match

stage0/src/Lean/Meta/Match/Match.lean

@@ -10,282 +10,44 @@ import Lean.Meta.Check
 import Lean.Meta.Closure
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.GeneralizeTelescope
-import Lean.Meta.Match.MatcherInfo
+import Lean.Meta.Match.Basic
 import Lean.Meta.Match.MVarRenaming
 import Lean.Meta.Match.CaseValues
-import Lean.Meta.Match.CaseArraySizes
 
 namespace Lean.Meta.Match
 
-inductive Pattern : Type :=
-  | inaccessible (e : Expr) : Pattern
-  | var          (fvarId : FVarId) : Pattern
-  | ctor         (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern) : Pattern
-  | val          (e : Expr) : Pattern
-  | arrayLit     (type : Expr) (xs : List Pattern) : Pattern
-  | as           (varId : FVarId) (p : Pattern) : Pattern
-
-namespace Pattern
-
-instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩
-
-partial def toMessageData : Pattern → MessageData
-  | inaccessible e         => m!".({e})"
-  | var varId              => mkFVar varId
-  | ctor ctorName _ _ []   => ctorName
-  | ctor ctorName _ _ pats => m!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
-  | val e                  => e
-  | arrayLit _ pats        => m!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
-  | as varId p             => m!"{mkFVar varId}@{toMessageData p}"
-
-partial def toExpr : Pattern → MetaM Expr
-  | inaccessible e                 => pure e
-  | var fvarId                     => pure $ mkFVar fvarId
-  | val e                          => pure e
-  | as _ p                         => toExpr p
-  | arrayLit type xs               => do
-    let xs ← xs.mapM toExpr;
-    mkArrayLit type xs
-  | ctor ctorName us params fields => do
-    let fields ← fields.mapM toExpr;
-    pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray
-
-/- Apply the free variable substitution `s` to the given pattern -/
-partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern
-  | inaccessible e  => inaccessible $ s.apply e
-  | ctor n us ps fs => ctor n us (ps.map s.apply) $ fs.map (applyFVarSubst s)
-  | val e           => val $ s.apply e
-  | arrayLit t xs   => arrayLit (s.apply t) $ xs.map (applyFVarSubst s)
-  | var fvarId      => match s.find? fvarId with
-    | some e => inaccessible e
-    | none   => var fvarId
-  | as fvarId p     => match s.find? fvarId with
-    | none   => as fvarId $ applyFVarSubst s p
-    | some _ => applyFVarSubst s p
-
-def replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern :=
-  let s : FVarSubst := {}
-  p.applyFVarSubst (s.insert fvarId v)
-
-partial def hasExprMVar : Pattern → Bool
-  | inaccessible e => e.hasExprMVar
-  | ctor _ _ ps fs => ps.any (·.hasExprMVar) || fs.any hasExprMVar
-  | val e          => e.hasExprMVar
-  | as _ p         => hasExprMVar p
-  | arrayLit t xs  => t.hasExprMVar || xs.any hasExprMVar
-  | _              => false
-
-end Pattern
-
-partial def instantiatePatternMVars : Pattern → MetaM Pattern
-  | Pattern.inaccessible e      => return Pattern.inaccessible (← instantiateMVars e)
-  | Pattern.val e               => return Pattern.val (← instantiateMVars e)
-  | Pattern.ctor n us ps fields => return Pattern.ctor n us (← ps.mapM instantiateMVars) (← fields.mapM instantiatePatternMVars)
-  | Pattern.as x p              => return Pattern.as x (← instantiatePatternMVars p)
-  | Pattern.arrayLit t xs       => return Pattern.arrayLit (← instantiateMVars t) (← xs.mapM instantiatePatternMVars)
-  | p                   => return p
-
-structure AltLHS :=
-  (ref        : Syntax)
-  (fvarDecls  : List LocalDecl) -- Free variables used in the patterns.
-  (patterns   : List Pattern)   -- We use `List Pattern` since we have nary match-expressions.
-
-def instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS :=
-  return { altLHS with
-    fvarDecls := (← altLHS.fvarDecls.mapM instantiateLocalDeclMVars),
-    patterns  := (← altLHS.patterns.mapM instantiatePatternMVars)
-  }
-
-structure Alt :=
-  (ref       : Syntax)
-  (idx       : Nat) -- for generating error messages
-  (rhs       : Expr)
-  (fvarDecls : List LocalDecl)
-  (patterns  : List Pattern)
-
-namespace Alt
-
-instance : Inhabited Alt := ⟨⟨arbitrary _, 0, arbitrary _, [], []⟩⟩
-
-partial def toMessageData (alt : Alt) : MetaM MessageData := do
-  withExistingLocalDecls alt.fvarDecls do
-    let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")"
-    let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs
-    addMessageContext msg
-
-def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
-  { alt with
-    patterns  := alt.patterns.map fun p => p.applyFVarSubst s,
-    fvarDecls := alt.fvarDecls.map fun d => d.applyFVarSubst s,
-    rhs       := alt.rhs.applyFVarSubst s }
-
-def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
-  { alt with
-    patterns  := alt.patterns.map fun p => p.replaceFVarId fvarId v,
-    fvarDecls :=
-      let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId
-      decls.map $ replaceFVarIdAtLocalDecl fvarId v,
-    rhs       := alt.rhs.replaceFVarId fvarId v }
-
-/-
-  Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`.
-  This extra check is necessary when performing dependent elimination and inaccessible terms have been used.
-  For example, consider the following code fragment:
-
-```
-inductive Vec (α : Type u) : Nat → Type u :=
-  | nil : Vec α 0
-  | cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
-
-inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop :=
-  | nil   : VecPred P Vec.nil
-  | cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
-
-theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-  | _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
-```
-Recall that `_` in a pattern can be elaborated into pattern variable or an inaccessible term.
-The elaborator uses an inaccessible term when typing constraints restrict its value.
-Thus, in the example above, the `_` at `Vec.cons head _` becomes the inaccessible pattern `.(Vec.nil)`
-because the type ascription `(w : VecPred P Vec.nil)` propagates typing constraints that restrict its value to be `Vec.nil`.
-After elaboration the alternative becomes:
-```
-  | .(0), @Vec.cons .(α) .(0) head .(Vec.nil), @VecPred.cons .(α) .(P) .(0) .(head) .(Vec.nil) h w => ⟨head, h⟩
-```
-where
-```
-(head : α), (h: P head), (w : VecPred P Vec.nil)
-```
-Then, when we process this alternative in this module, the following check will detect that
-`w` has type `VecPred P Vec.nil`, when it is supposed to have type `VecPred P tail`.
-Note that if we had written
-```
-theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-  | _, Vec.cons head Vec.nil, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
-```
-we would get the easier to digest error message
-```
-missing cases:
-_, (Vec.cons _ _ (Vec.cons _ _ _)), _
-```
--/
-def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt := do
-  match alt.fvarDecls.find? fun (fvarDecl : LocalDecl) => fvarDecl.fvarId == fvarId with
-  | none          => throwErrorAt alt.ref "unknown free pattern variable"
-  | some fvarDecl => do
-    let vType ← inferType v
-    unless (← isDefEqGuarded fvarDecl.type vType) do
-      withExistingLocalDecls alt.fvarDecls do
-        throwErrorAt alt.ref $
-          m!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
-    pure $ replaceFVarId fvarId v alt
-
-end Alt
-
-inductive Example :=
-  | var        : FVarId → Example
-  | underscore : Example
-  | ctor       : Name → List Example → Example
-  | val        : Expr → Example
-  | arrayLit   : List Example → Example
-
-namespace Example
-
-partial def replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example
-  | var x        => if x == fvarId then ex else var x
-  | ctor n exs   => ctor n $ exs.map (replaceFVarId fvarId ex)
-  | arrayLit exs => arrayLit $ exs.map (replaceFVarId fvarId ex)
-  | ex           => ex
-
-partial def applyFVarSubst (s : FVarSubst) : Example → Example
-  | var fvarId =>
-    match s.get fvarId with
-    | Expr.fvar fvarId' _ => var fvarId'
-    | _                   => underscore
-  | ctor n exs   => ctor n $ exs.map (applyFVarSubst s)
-  | arrayLit exs => arrayLit $ exs.map (applyFVarSubst s)
-  | ex           => ex
-
-partial def varsToUnderscore : Example → Example
-  | var x        => underscore
-  | ctor n exs   => ctor n $ exs.map varsToUnderscore
-  | arrayLit exs => arrayLit $ exs.map varsToUnderscore
-  | ex           => ex
-
-partial def toMessageData : Example → MessageData
-  | var fvarId        => mkFVar fvarId
-  | ctor ctorName []  => mkConst ctorName
-  | ctor ctorName exs => "(" ++ mkConst ctorName ++ exs.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil ++ ")"
-  | arrayLit exs      => "#" ++ MessageData.ofList (exs.map toMessageData)
-  | val e             => e
-  | underscore        => "_"
-
-end Example
-
-def examplesToMessageData (cex : List Example) : MessageData :=
-  MessageData.joinSep (cex.map (Example.toMessageData ∘ Example.varsToUnderscore)) ", "
-
-structure Problem :=
-  (mvarId        : MVarId)
-  (vars          : List Expr)
-  (alts          : List Alt)
-  (examples      : List Example)
-
-def withGoalOf {α} (p : Problem) (x : MetaM α) : MetaM α :=
-  withMVarContext p.mvarId x
-
-instance : Inhabited Problem := ⟨{ mvarId := arbitrary _, vars := [], alts := [], examples := []}⟩
-
-def Problem.toMessageData (p : Problem) : MetaM MessageData :=
-  withGoalOf p do
-    let alts ← p.alts.mapM Alt.toMessageData
-    let vars ← p.vars.mapM fun x => do let xType ← inferType x; pure (x ++ ":(" ++ xType ++ ")" : MessageData)
-    return "remaining variables: " ++ vars
-      ++ Format.line ++ "alternatives:" ++ indentD (MessageData.joinSep alts Format.line)
-      ++ Format.line ++ "examples: " ++ examplesToMessageData p.examples
-      ++ Format.line
-
-abbrev CounterExample := List Example
-
-def counterExampleToMessageData (cex : CounterExample) : MessageData :=
-  examplesToMessageData cex
-
-def counterExamplesToMessageData (cexs : List CounterExample) : MessageData :=
-  MessageData.joinSep (cexs.map counterExampleToMessageData) Format.line
-
-structure MatcherResult :=
-  (matcher         : Expr) -- The matcher. It is not just `Expr.const matcherName` because the type of the major premises may contain free variables.
-  (counterExamples : List CounterExample)
-  (unusedAltIdxs   : List Nat)
-
 /- The number of patterns in each AltLHS must be equal to majors.length -/
 private def checkNumPatterns (majors : Array Expr) (lhss : List AltLHS) : MetaM Unit := do
   let num := majors.size
   if lhss.any fun lhs => lhs.patterns.length != num then
     throwError "incorrect number of patterns"
 
-private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt → Array (Expr × Nat) → (List Alt → Array (Expr × Nat) → MetaM α) → MetaM α
-  | [],        alts, minors, k => k alts.reverse minors
-  | lhs::lhss, alts, minors, k => do
-    let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
-    let minorType ← withExistingLocalDecls lhs.fvarDecls do
-      let args ← lhs.patterns.toArray.mapM Pattern.toExpr
+/- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
+private def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt → Array (Expr × Nat) → MetaM α) : MetaM α :=
+  loop lhss [] #[]
+where
+  mkMinorType (xs : Array Expr) (lhs : AltLHS) : MetaM Expr :=
+    withExistingLocalDecls lhs.fvarDecls do
+      let args ← lhs.patterns.toArray.mapM (Pattern.toExpr · (annotate := true))
       let minorType := mkAppN motive args
       mkForallFVars xs minorType
-    let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
-    let idx       := alts.length
-    let minorName := (`h).appendIndexAfter (idx+1)
-    trace[Meta.Match.debug]! "minor premise {minorName} : {minorType}"
-    withLocalDeclD minorName minorType fun minor => do
-      let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
-      let minors := minors.push (minor, minorNumParams)
-      let fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars
-      let alts   := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts
-      withAltsAux motive lhss alts minors k
 
-/- Given a list of `AltLHS`, create a minor premise for each one, convert them into `Alt`, and then execute `k` -/
-private partial def withAlts {α} (motive : Expr) (lhss : List AltLHS) (k : List Alt → Array (Expr × Nat) → MetaM α) : MetaM α :=
-  withAltsAux motive lhss [] #[] k
+  loop (lhss : List AltLHS) (alts : List Alt) (minors : Array (Expr × Nat)) : MetaM α := do
+    match lhss with
+    | [] => k alts.reverse minors
+    | lhs::lhss =>
+      let xs := lhs.fvarDecls.toArray.map LocalDecl.toExpr
+      let minorType ← mkMinorType xs lhs
+      let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
+      let idx       := alts.length
+      let minorName := (`h).appendIndexAfter (idx+1)
+      trace[Meta.Match.debug]! "minor premise {minorName} : {minorType}"
+      withLocalDeclD minorName minorType fun minor => do
+        let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
+        let minors := minors.push (minor, minorNumParams)
+        let fvarDecls ← lhs.fvarDecls.mapM instantiateLocalDeclMVars
+        let alts   := { ref := lhs.ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := lhs.patterns : Alt } :: alts
+        loop lhss alts minors
 
 def assignGoalOf (p : Problem) (e : Expr) : MetaM Unit :=
   withGoalOf p (assignExprMVar p.mvarId e)
@@ -467,9 +229,7 @@ partial def unify (a : Expr) (b : Expr) : M Bool := do
       | Expr.fvar aFvarId _, b => assign aFvarId b
       | a, Expr.fvar bFVarId _ => assign bFVarId a
       | Expr.app aFn aArg _, Expr.app bFn bArg _ => unify aFn bFn <&&> unify aArg bArg
-      | _, _ =>
-        trace[Meta.Match.unify]! "unify failed @ {a} =?= {b}"
-        pure false
+      | _, _ => pure false
 
 end Unify
 
@@ -831,9 +591,8 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
     addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
     setInlineAttribute matcherName
     trace[Meta.Match.debug]! "matcher: {matcher}"
-    let unusedAltIdxs : List Nat := lhss.length.fold
-      (fun i r => if s.used.contains i then r else i::r)
-      []
+    let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
+      if s.used.contains i then r else i::r
     pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := unusedAltIdxs.reverse }
 
 end Match

stage0/src/Lean/Parser/Command.lean

@@ -47,17 +47,20 @@ def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
 def inferMod         := parser! atomic ("{" >> "}")
 def ctor             := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
-def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
-def classInductive   := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
+def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
+def classInductive   := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
 def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
 def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
 def structInstBinder     := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
-def structFields         := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder))
+def structSimpleBinder   := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
+def structFields         := parser! manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
 def structCtor           := parser! atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
 def structureTk          := parser! "structure "
 def classTk              := parser! "class "
 def «extends»            := parser! " extends " >> sepBy1 termParser ", "
-def «structure»          := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
+def «structure»          := parser!
+    (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType
+    >> optional ((" := " <|> " where ") >> optional structCtor >> structFields)
 @[builtinCommandParser] def declaration := parser!
 declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 

stage0/stdlib/Init/Control/Basic.c

@@ -36,6 +36,7 @@ lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_bool_match__1(lean_object*);
 lean_object* l_myMacro____x40_Init_Control_Basic___hyg_75____closed__6;
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 lean_object* l_controlAt(lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_andM_match__1___rarg(uint8_t, lean_object*, lean_object*);
@@ -134,7 +135,6 @@ lean_object* l_myMacro____x40_Init_Control_Basic___hyg_75____closed__7;
 lean_object* l_andM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_andM(lean_object*, lean_object*);
 lean_object* l___kind_term____x40_Init_Control_Basic___hyg_38____closed__6;
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_guard(lean_object*);
 lean_object* l_optional(lean_object*);
 lean_object* l_orM(lean_object*, lean_object*);
@@ -686,7 +686,7 @@ static lean_object* _init_l_instToBoolBool() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 return x_1;
 }
 }

stage0/stdlib/Init/Meta.c

@@ -122,6 +122,7 @@ lean_object* l_Lean_Syntax_setTailInfo(lean_object*, lean_object*);
 lean_object* l_Lean_instQuoteArray(lean_object*);
 lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instQuoteProd_match__1(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 lean_object* l_Lean_Syntax_identToStrLit(lean_object*);
 lean_object* l_Array_filterSepElemsM___at_Array_filterSepElems___spec__1(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6336____closed__5;
@@ -487,7 +488,6 @@ lean_object* l_Lean_Syntax_expandInterpolatedStr___boxed(lean_object*, lean_obje
 lean_object* l_Lean_mkSepArray___closed__1;
 lean_object* l___private_Init_Meta_0__Lean_Syntax_decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_Syntax_decodeQuotedChar_match__4(lean_object*);
 lean_object* l_Lean_mkSepArray___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isNone_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -8372,7 +8372,7 @@ static lean_object* _init_l_Lean_instQuoteSyntax() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 return x_1;
 }
 }

stage0/stdlib/Init/Prelude.c

@@ -119,6 +119,7 @@ lean_object* l_List_lengthAux___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_idDelta___rarg(lean_object*);
 lean_object* l_ReaderT_read___at_Lean_Macro_instMonadRefMacroM___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isOfKind___boxed(lean_object*, lean_object*);
+lean_object* l_Applicative_seqRight___default___rarg___closed__2;
 lean_object* l_instInhabitedDepArrow___rarg(lean_object*, lean_object*);
 lean_object* l_instDecidableOr_match__2___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_EStateM_dummyRestore___rarg(lean_object*, lean_object*);
@@ -688,7 +689,7 @@ lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux___boxed(lean_o
 lean_object* l_UInt16_ofNatCore___boxed(lean_object*, lean_object*);
 lean_object* lean_array_to_list(lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
-lean_object* l_instOfNatNat;
+lean_object* l_instOfNatNat(lean_object*);
 size_t lean_usize_mix_hash(size_t, size_t);
 lean_object* l_UInt32_size;
 lean_object* l_Lean_instInhabitedMacroScopesView___closed__1;
@@ -766,8 +767,8 @@ lean_object* l_instInhabitedArrow(lean_object*, lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 uint8_t l_instDecidableOr___rarg(uint8_t, uint8_t);
 lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
-lean_object* l_instOfNatNat___closed__1;
 lean_object* l___private_Init_Prelude_0__Lean_extractImported_match__1(lean_object*);
+lean_object* l_instOfNatNat___boxed(lean_object*);
 lean_object* l_Lean_MonadQuotation_addMacroScope(lean_object*);
 uint32_t lean_uint32_of_nat(lean_object*);
 lean_object* l_instInhabitedSort;
@@ -2035,20 +2036,20 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_instOfNatNat___closed__1() {
+lean_object* l_instOfNatNat(lean_object* x_1) {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_id___rarg___boxed), 1, 0);
+lean_inc(x_1);
 return x_1;
 }
 }
-static lean_object* _init_l_instOfNatNat() {
+lean_object* l_instOfNatNat___boxed(lean_object* x_1) {
 _start:
 {
-lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
-return x_1;
+lean_object* x_2; 
+x_2 = l_instOfNatNat(x_1);
+lean_dec(x_1);
+return x_2;
 }
 }
 static lean_object* _init_l_instInhabitedNat() {
@@ -4475,8 +4476,16 @@ return x_2;
 static lean_object* _init_l_Applicative_seqRight___default___rarg___closed__1() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_id___rarg___boxed), 1, 0);
+return x_1;
+}
+}
+static lean_object* _init_l_Applicative_seqRight___default___rarg___closed__2() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 x_2 = lean_alloc_closure((void*)(l_Function_const___rarg___boxed), 2, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
@@ -4489,7 +4498,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
 x_6 = lean_ctor_get(x_1, 0);
 lean_inc(x_6);
 lean_dec(x_1);
-x_7 = l_Applicative_seqRight___default___rarg___closed__1;
+x_7 = l_Applicative_seqRight___default___rarg___closed__2;
 x_8 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_7, x_4);
 x_9 = lean_apply_4(x_2, lean_box(0), lean_box(0), x_8, x_5);
 return x_9;
@@ -11004,10 +11013,6 @@ lean_mark_persistent(l_Unit_unit);
 l_instInhabitedSort = _init_l_instInhabitedSort();
 l_instInhabitedPointedType = _init_l_instInhabitedPointedType();
 lean_mark_persistent(l_instInhabitedPointedType);
-l_instOfNatNat___closed__1 = _init_l_instOfNatNat___closed__1();
-lean_mark_persistent(l_instOfNatNat___closed__1);
-l_instOfNatNat = _init_l_instOfNatNat();
-lean_mark_persistent(l_instOfNatNat);
 l_instInhabitedNat = _init_l_instInhabitedNat();
 lean_mark_persistent(l_instInhabitedNat);
 l_instAddNat___closed__1 = _init_l_instAddNat___closed__1();
@@ -11077,6 +11082,8 @@ l_Applicative_seqLeft___default___rarg___closed__1 = _init_l_Applicative_seqLeft
 lean_mark_persistent(l_Applicative_seqLeft___default___rarg___closed__1);
 l_Applicative_seqRight___default___rarg___closed__1 = _init_l_Applicative_seqRight___default___rarg___closed__1();
 lean_mark_persistent(l_Applicative_seqRight___default___rarg___closed__1);
+l_Applicative_seqRight___default___rarg___closed__2 = _init_l_Applicative_seqRight___default___rarg___closed__2();
+lean_mark_persistent(l_Applicative_seqRight___default___rarg___closed__2);
 l_ReaderT_instMonadLiftReaderT___closed__1 = _init_l_ReaderT_instMonadLiftReaderT___closed__1();
 lean_mark_persistent(l_ReaderT_instMonadLiftReaderT___closed__1);
 l_EStateM_instMonadEStateM___closed__1 = _init_l_EStateM_instMonadEStateM___closed__1();

stage0/stdlib/Init/System/IO.c

@@ -20,7 +20,6 @@ lean_object* l_IO_getStdin___rarg___closed__1;
 lean_object* l_MonadExcept_orelse___at_instOrElseEIO___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_putStrLn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_getStdout(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__12;
 lean_object* l_IO_FS_withIsolatedStreams___rarg(lean_object*, lean_object*);
 lean_object* l_allocprof___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instEvalUnit___rarg(uint8_t, lean_object*);
@@ -48,7 +47,6 @@ lean_object* lean_io_error_to_string(lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_println(lean_object*);
 lean_object* l_IO_Prim_fopenFlags_match__1(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__10;
 lean_object* l_IO_currentDir___rarg___closed__1;
 lean_object* l_IO_Prim_getStderr___boxed(lean_object*);
 lean_object* l_IO_Prim_fopenFlags___closed__12;
@@ -57,6 +55,7 @@ lean_object* l_IO_hasFinished___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_withFile___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_io_is_dir(lean_object*, lean_object*);
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__7;
 lean_object* l_IO_FS_Handle_putStr___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_instMonadFinallyEIO(lean_object*);
 lean_object* l_IO_instMonadLiftSTRealWorldEIO_match__2(lean_object*, lean_object*);
@@ -68,6 +67,7 @@ lean_object* l_IO_FS_Stream_putStrLn___rarg(lean_object*, lean_object*, lean_obj
 lean_object* l_EStateM_tryCatch___at_IO_FS_withIsolatedStreams___spec__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_prim_handle_put_str(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_3____closed__13;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__14;
 lean_object* l_IO_waitAny___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_getEnv___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FileRight_user___default___closed__1;
@@ -75,11 +75,10 @@ lean_object* l_Lean_instEval___rarg(lean_object*, lean_object*, uint8_t, lean_ob
 lean_object* l_IO_toEIO(lean_object*);
 lean_object* l_IO_FS_Handle_getLine___rarg(lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__11;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__10;
 lean_object* l_Lean_instEvalIO___rarg(lean_object*, lean_object*, uint8_t, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__19;
 lean_object* l_IO_Prim_getStdout___boxed(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__7;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 lean_object* l_Monad_seqRight___default___rarg___lambda__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
@@ -94,7 +93,6 @@ lean_object* l_IO_FS_Stream_ofBuffer___elambda__5(lean_object*);
 lean_object* l_Lean_instEvalUnit(lean_object*);
 lean_object* l_IO_FS_Handle_flush___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_instEvalUnit___rarg___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
 lean_object* l_ST_Prim_mkRef___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_withStdin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Prim_Handle_mk___boxed(lean_object*, lean_object*, lean_object*);
@@ -105,6 +103,7 @@ lean_object* lean_array_get_size(lean_object*);
 lean_object* l_IO_withStderr___at_IO_FS_withIsolatedStreams___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 extern lean_object* l_Lean_interpolatedStrKind;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5739____closed__11;
 lean_object* l_IO_Process_SpawnArgs_args___default;
 uint32_t l_IO_AccessRight_flags___closed__6;
@@ -112,6 +111,7 @@ lean_object* l_IO_FS_Handle_readToEnd___rarg(lean_object*, lean_object*, lean_ob
 lean_object* l_IO_ofExcept_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_instMonadLiftSTRealWorldEIO_match__1___boxed(lean_object*, lean_object*);
 lean_object* l_IO_isDir(lean_object*);
+lean_object* l_IO_sleep(uint32_t, lean_object*);
 lean_object* l_IO_Prim_setStdout___boxed(lean_object*, lean_object*);
 lean_object* l_EIO_catchExceptions_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_withIsolatedStreams___rarg___closed__3;
@@ -136,14 +136,13 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_8168____closed__8;
 lean_object* l_IO_eprintln(lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___lambda__1(lean_object*, lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
 lean_object* l_IO_FS_Stream_ofHandle___elambda__5(lean_object*, lean_object*);
 lean_object* l_IO_Prim_Handle_isEof___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__17;
 lean_object* l_IO_instMonadLiftSTRealWorldEIO(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer(lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_setStderr(lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__7;
 lean_object* lean_io_bind_task(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_eprint___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_withStdout___at_IO_FS_withIsolatedStreams___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -157,35 +156,37 @@ extern lean_object* l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____clo
 lean_object* l_IO_FS_withIsolatedStreams___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* lean_io_as_task(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_AccessRight_flags___boxed(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__9;
 lean_object* l_IO_Prim_realPath___boxed(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__2___boxed(lean_object*, lean_object*);
 extern lean_object* l_ByteArray_empty;
 lean_object* l_IO_appDir(lean_object*);
 lean_object* lean_io_eprintln(lean_object*, lean_object*);
 lean_object* l_EIO_toIO___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__18;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__5;
 uint32_t l_IO_AccessRight_flags___closed__1;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__2;
 uint32_t l_IO_AccessRight_flags___closed__9;
 lean_object* l_IO_appPath___rarg(lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
+lean_object* l_IO_sleep___lambda__1(lean_object*, lean_object*);
 uint32_t l_IO_AccessRight_flags___closed__2;
 lean_object* l_IO_Process_SpawnArgs_env___default;
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521_;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__6;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535_;
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__5;
 lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Task_Priority_dedicated;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
 lean_object* l_IO_eprintln___at___private_Init_System_IO_0__IO_eprintlnAux___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___lambda__1___boxed(lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__2;
 lean_object* lean_get_set_stderr(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_read___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__1;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__1;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__3;
 uint32_t l_IO_AccessRight_flags___closed__4;
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__15;
 lean_object* l_IO_getStderr___rarg___closed__1;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__8;
 lean_object* l_IO_mkRef___at_IO_FS_withIsolatedStreams___spec__1___rarg(lean_object*, lean_object*);
 lean_object* lean_io_current_dir(lean_object*);
 lean_object* l_IO_Prim_fopenFlags___closed__10;
@@ -196,18 +197,17 @@ lean_object* l_IO_FS_Stream_ofBuffer_match__1(lean_object*);
 lean_object* l_IO_Process_run___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_putStrLn(lean_object*);
 lean_object* lean_io_wait(lean_object*, lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__6;
 lean_object* l_IO_print___at_IO_println___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_write___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_readToEnd_read___at_IO_Process_output___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_withStdin___at_IO_FS_withIsolatedStreams___spec__8(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_tryCatch___at_IO_FS_withIsolatedStreams___spec__2(lean_object*);
 lean_object* l_IO_getStderr___rarg(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__1;
 lean_object* lean_io_realpath(lean_object*, lean_object*);
 lean_object* l_System_FilePath_dirName(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__5;
 lean_object* l_IO_getStdout___rarg(lean_object*);
+lean_object* lean_dbg_sleep(uint32_t, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5739____closed__20;
 lean_object* l_IO_Prim_fopenFlags(uint8_t, uint8_t);
 lean_object* l_IO_eprintln___rarg(lean_object*, lean_object*, lean_object*);
@@ -226,6 +226,7 @@ extern lean_object* l___kind_term____x40_Init_Notation___hyg_5672____closed__9;
 lean_object* l_EStateM_instMonadFinallyEStateM(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__2___boxed(lean_object*, lean_object*);
 lean_object* l_IO_initializing___boxed(lean_object*);
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_1011____closed__7;
 lean_object* lean_stream_of_handle(lean_object*);
 extern lean_object* l_instMonadExceptOfEST___closed__2;
@@ -239,6 +240,7 @@ lean_object* l_IO_FS_lines_read(lean_object*);
 lean_object* l_IO_Prim_Handle_getLine___boxed(lean_object*, lean_object*);
 lean_object* l_IO_FS_lines_read___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_mk___rarg(lean_object*, lean_object*, uint8_t, uint8_t);
+lean_object* l_IO_sleep___lambda__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_instMonadEST___closed__1;
 lean_object* l_IO_println___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Process_spawn___boxed(lean_object*, lean_object*);
@@ -246,6 +248,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__8;
 lean_object* l_IO_getStdout___rarg___closed__1;
 lean_object* l_IO_FS_Stream_ofHandle___elambda__5___boxed(lean_object*, lean_object*);
 lean_object* l_IO_getStdin___rarg(lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__6;
 lean_object* l_IO_fileExists___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_readToEnd_read(lean_object*);
 lean_object* l_IO_FS_Handle_isEof(lean_object*);
@@ -254,6 +257,8 @@ lean_object* l_IO_realPath___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_Buffer_data___default;
 lean_object* l_IO_Prim_fopenFlags___closed__6;
 lean_object* l_IO_Prim_appPath___boxed(lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 lean_object* l_IO_setStdin___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FileRight_flags___boxed(lean_object*);
 lean_object* l_instInhabitedEIO(lean_object*);
@@ -261,7 +266,6 @@ lean_object* l_IO_FS_Stream_ofBuffer_match__1___rarg(lean_object*, lean_object*,
 uint32_t l_IO_AccessRight_flags___closed__11;
 lean_object* l_IO_setStdin___at_IO_FS_withIsolatedStreams___spec__9(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_read(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__6;
 lean_object* lean_io_has_finished(lean_object*, lean_object*);
 lean_object* l_String_dropRight(lean_object*, lean_object*);
 lean_object* l_EIO_catchExceptions(lean_object*, lean_object*);
@@ -271,17 +275,17 @@ lean_object* l_IO_setStderr___at_IO_FS_withIsolatedStreams___spec__4(lean_object
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_setStdout___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__2(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__5;
 lean_object* l_IO_Process_run(lean_object*, lean_object*);
 uint8_t l_IO_AccessRight_write___default;
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__6(lean_object*, lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__2;
 lean_object* l_IO_ofExcept___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
 extern lean_object* l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____closed__6;
 lean_object* l_IO_Prim_fileExists___boxed(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569_(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583_(lean_object*, lean_object*, lean_object*);
 uint8_t l_IO_Process_StdioConfig_stdout___default;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__11;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__8;
 lean_object* l_IO_Process_Stdio_toHandleType_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_readToEnd_read___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_realPath(lean_object*);
@@ -289,33 +293,32 @@ lean_object* lean_io_prim_handle_write(lean_object*, lean_object*, lean_object*)
 lean_object* l_IO_FS_withIsolatedStreams___rarg___closed__1;
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_ofExcept(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__15;
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__4;
 lean_object* lean_io_file_exists(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__14;
 uint8_t l_UInt32_decEq(uint32_t, uint32_t);
 lean_object* lean_io_check_canceled(lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__4(lean_object*, size_t, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___elambda__4(lean_object*, size_t, lean_object*);
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__2;
 lean_object* l_IO_currentDir(lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__1;
 lean_object* l_IO_Prim_isDir___boxed(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_putStr(lean_object*);
 lean_object* l_IO_Prim_setAccessRights___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_isDir___rarg(lean_object*, lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__18;
 lean_object* l_IO_getEnv(lean_object*);
 lean_object* l_Lean_instEvalIO___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_sleep___boxed(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_instReprUnit___closed__1;
 lean_object* l_unsafeEIO___rarg(lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__17;
 lean_object* lean_string_to_utf8(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__4;
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__3;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__8;
 lean_object* l_ByteArray_findIdx_x3f_loop___at_IO_FS_Stream_ofBuffer___elambda__2___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_IO_ofExcept_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_process_child_wait(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__8;
 lean_object* l_IO_lazyPure(lean_object*);
 lean_object* l_IO_setStderr___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_mk___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -328,6 +331,7 @@ lean_object* l_IO_Prim_fopenFlags___closed__5;
 lean_object* lean_get_stdout(lean_object*);
 lean_object* l_IO_FS_Stream_ofHandle___elambda__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Prim_iterate_match__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__9;
 lean_object* l_IO_ofExcept___at_IO_Process_output___spec__3(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5739____closed__22;
 lean_object* l_IO_withStderr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -340,11 +344,11 @@ uint32_t l_IO_AccessRight_flags(lean_object*);
 lean_object* l_unsafeIO(lean_object*);
 lean_object* l_IO_Prim_fopenFlags_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Prim_fopenFlags___closed__3;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_object* l_IO_FS_withIsolatedStreams___rarg___lambda__2(lean_object*, lean_object*);
 extern lean_object* l_Lean_Name_hasMacroScopes___closed__1;
 lean_object* l_IO_withStdin___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_checkCanceled___boxed(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__7;
 lean_object* l_IO_FileRight_group___default;
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_toEIO___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -361,6 +365,7 @@ lean_object* lean_get_set_stdin(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_getLine___at_IO_Process_output___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_EStateM_instInhabitedEStateM___rarg(lean_object*, lean_object*);
 lean_object* l_instOrElseEIO(lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__19;
 lean_object* l_IO_eprint___at_IO_eprintln___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_appDir___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_read___rarg(lean_object*, lean_object*, lean_object*);
@@ -383,19 +388,17 @@ lean_object* l_IO_mkRef(lean_object*, lean_object*);
 uint8_t l_IO_Process_StdioConfig_stderr___default;
 uint8_t lean_byte_array_get(lean_object*, lean_object*);
 lean_object* l_IO_getStderr(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
 lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object*);
 lean_object* l_IO_ofExcept___at_IO_Process_output___spec__3___rarg(lean_object*, lean_object*);
 uint8_t l_IO_Process_StdioConfig_stdin___default;
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__20;
 extern lean_object* l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____closed__7;
 lean_object* l_IO_Prim_fopenFlags___closed__8;
 lean_object* l_IO_Prim_Handle_putStr___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_IO_withStdout(lean_object*);
-lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__11;
 lean_object* l_timeit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_app_dir(lean_object*);
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__20;
 lean_object* l_IO_FS_Handle_isEof___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_flush(lean_object*);
 uint32_t l_IO_AccessRight_flags___closed__12;
@@ -414,6 +417,7 @@ lean_object* l_IO_instMonadLiftSTRealWorldEIO___rarg(lean_object*, lean_object*)
 lean_object* lean_usize_to_nat(size_t);
 lean_object* l_Lean_instEval__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_lines(lean_object*);
+lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__11;
 lean_object* l_Functor_discard___at_IO_FS_withIsolatedStreams___spec__5(lean_object*, lean_object*);
 lean_object* l_IO_fileExists(lean_object*);
 lean_object* l_Lean_runEval___rarg(lean_object*, lean_object*, lean_object*);
@@ -433,6 +437,7 @@ lean_object* lean_io_prim_handle_mk(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_ofBuffer___closed__1;
 lean_object* l_IO_getStdout___at_IO_print___spec__1(lean_object*);
 lean_object* l_IO_appDir___rarg(lean_object*, lean_object*);
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__12;
 lean_object* l_IO_currentDir___rarg(lean_object*);
 lean_object* l_IO_setStdout___at_IO_FS_withIsolatedStreams___spec__7(lean_object*, lean_object*);
 lean_object* lean_task_get_own(lean_object*);
@@ -1069,6 +1074,46 @@ x_2 = lean_alloc_closure((void*)(l_IO_lazyPure___rarg), 2, 0);
 return x_2;
 }
 }
+lean_object* l_IO_sleep___lambda__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_box(0);
+x_4 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_4, 0, x_3);
+lean_ctor_set(x_4, 1, x_1);
+return x_4;
+}
+}
+lean_object* l_IO_sleep(uint32_t x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_alloc_closure((void*)(l_IO_sleep___lambda__1___boxed), 2, 1);
+lean_closure_set(x_3, 0, x_2);
+x_4 = lean_dbg_sleep(x_1, x_3);
+return x_4;
+}
+}
+lean_object* l_IO_sleep___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_IO_sleep___lambda__1(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
+lean_object* l_IO_sleep___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint32_t x_3; lean_object* x_4; 
+x_3 = lean_unbox_uint32(x_1);
+lean_dec(x_1);
+x_4 = l_IO_sleep(x_3, x_2);
+return x_4;
+}
+}
 lean_object* l_IO_asTask___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -6320,7 +6365,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_runEval___rarg), 3, 0);
 return x_2;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__1() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -6328,17 +6373,17 @@ x_1 = lean_mk_string("System");
 return x_1;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__2() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__7;
-x_2 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__1;
+x_2 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__3() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -6346,37 +6391,37 @@ x_1 = lean_mk_string("IO");
 return x_1;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__4() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__2;
-x_2 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__2;
+x_2 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__5() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__4;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__4;
 x_2 = l_Lean_Name_hasMacroScopes___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__6() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__5;
-x_2 = lean_unsigned_to_nat(2521u);
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__5;
+x_2 = lean_unsigned_to_nat(2535u);
 x_3 = lean_name_mk_numeral(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__7() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__7() {
 _start:
 {
 lean_object* x_1; 
@@ -6384,17 +6429,17 @@ x_1 = lean_mk_string("println! ");
 return x_1;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__8() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__7;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__7;
 x_2 = lean_alloc_ctor(5, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__9() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
@@ -6408,13 +6453,13 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__10() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
-x_2 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__8;
-x_3 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
+x_2 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__8;
+x_3 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -6422,13 +6467,13 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__11() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__6;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__6;
 x_2 = lean_unsigned_to_nat(1023u);
-x_3 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__10;
+x_3 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__10;
 x_4 = lean_alloc_ctor(3, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -6436,15 +6481,15 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2521_() {
+static lean_object* _init_l___kind_term____x40_Init_System_IO___hyg_2535_() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__11;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__11;
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__1() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -6452,22 +6497,22 @@ x_1 = lean_mk_string("IO.println");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__2() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__1;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__1;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__3() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__1;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__1;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__2;
+x_3 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__2;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -6475,17 +6520,17 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__4() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_2 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__5() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -6493,56 +6538,56 @@ x_1 = lean_mk_string("println");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__6() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__5;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__5;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__7() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__6;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__6;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__8() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__7;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__7;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__9() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__10() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_1 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__9;
+x_3 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__9;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -6550,31 +6595,31 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__11() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__12() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__12() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__11;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__11;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__13() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__13() {
 _start:
 {
 lean_object* x_1; 
@@ -6582,22 +6627,22 @@ x_1 = lean_mk_string("Unit");
 return x_1;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__14() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__14() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__15() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__15() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__14;
+x_3 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__14;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -6605,41 +6650,41 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__16() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__16() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__17() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__17() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__18() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__18() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__17;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__17;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__19() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__19() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -6651,21 +6696,21 @@ lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__20() {
+static lean_object* _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__20() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Array_empty___closed__1;
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__19;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__19;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_myMacro____x40_Init_System_IO___hyg_2569_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_myMacro____x40_Init_System_IO___hyg_2583_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
-x_4 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__6;
+x_4 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__6;
 lean_inc(x_1);
 x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
 if (x_5 == 0)
@@ -6718,13 +6763,13 @@ lean_inc(x_19);
 x_20 = lean_ctor_get(x_2, 1);
 lean_inc(x_20);
 lean_dec(x_2);
-x_21 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__6;
+x_21 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__6;
 lean_inc(x_19);
 lean_inc(x_20);
 x_22 = l_Lean_addMacroScope(x_20, x_21, x_19);
 x_23 = l_Lean_instInhabitedSourceInfo___closed__1;
-x_24 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__3;
-x_25 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__8;
+x_24 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__3;
+x_25 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__8;
 x_26 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_26, 0, x_23);
 lean_ctor_set(x_26, 1, x_24);
@@ -6743,22 +6788,22 @@ x_34 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_34, 0, x_33);
 lean_ctor_set(x_34, 1, x_32);
 x_35 = lean_array_push(x_27, x_34);
-x_36 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_36 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_inc(x_19);
 lean_inc(x_20);
 x_37 = l_Lean_addMacroScope(x_20, x_36, x_19);
-x_38 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
-x_39 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__12;
+x_38 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
+x_39 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__12;
 x_40 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_40, 0, x_23);
 lean_ctor_set(x_40, 1, x_38);
 lean_ctor_set(x_40, 2, x_37);
 lean_ctor_set(x_40, 3, x_39);
 x_41 = lean_array_push(x_27, x_40);
-x_42 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_42 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_43 = l_Lean_addMacroScope(x_20, x_42, x_19);
-x_44 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__15;
-x_45 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__18;
+x_44 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__15;
+x_45 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__18;
 x_46 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_46, 0, x_23);
 lean_ctor_set(x_46, 1, x_44);
@@ -6807,13 +6852,13 @@ lean_inc(x_66);
 x_67 = lean_ctor_get(x_2, 1);
 lean_inc(x_67);
 lean_dec(x_2);
-x_68 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__6;
+x_68 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__6;
 lean_inc(x_66);
 lean_inc(x_67);
 x_69 = l_Lean_addMacroScope(x_67, x_68, x_66);
 x_70 = l_Lean_instInhabitedSourceInfo___closed__1;
-x_71 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__3;
-x_72 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__8;
+x_71 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__3;
+x_72 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__8;
 x_73 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_73, 0, x_70);
 lean_ctor_set(x_73, 1, x_71);
@@ -6821,7 +6866,7 @@ lean_ctor_set(x_73, 2, x_69);
 lean_ctor_set(x_73, 3, x_72);
 x_74 = l_Array_empty___closed__1;
 x_75 = lean_array_push(x_74, x_73);
-x_76 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__20;
+x_76 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__20;
 x_77 = lean_array_push(x_76, x_15);
 x_78 = l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____closed__6;
 x_79 = lean_alloc_ctor(1, 2, 0);
@@ -6852,22 +6897,22 @@ x_95 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_95, 0, x_94);
 lean_ctor_set(x_95, 1, x_93);
 x_96 = lean_array_push(x_74, x_95);
-x_97 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_97 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_inc(x_66);
 lean_inc(x_67);
 x_98 = l_Lean_addMacroScope(x_67, x_97, x_66);
-x_99 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
-x_100 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__12;
+x_99 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
+x_100 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__12;
 x_101 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_101, 0, x_70);
 lean_ctor_set(x_101, 1, x_99);
 lean_ctor_set(x_101, 2, x_98);
 lean_ctor_set(x_101, 3, x_100);
 x_102 = lean_array_push(x_74, x_101);
-x_103 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_103 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_104 = l_Lean_addMacroScope(x_67, x_103, x_66);
-x_105 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__15;
-x_106 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__18;
+x_105 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__15;
+x_106 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__18;
 x_107 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_107, 0, x_70);
 lean_ctor_set(x_107, 1, x_105);
@@ -7035,70 +7080,70 @@ l_IO_FS_withIsolatedStreams___rarg___closed__2 = _init_l_IO_FS_withIsolatedStrea
 lean_mark_persistent(l_IO_FS_withIsolatedStreams___rarg___closed__2);
 l_IO_FS_withIsolatedStreams___rarg___closed__3 = _init_l_IO_FS_withIsolatedStreams___rarg___closed__3();
 lean_mark_persistent(l_IO_FS_withIsolatedStreams___rarg___closed__3);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__1 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__1();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__1);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__2 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__2();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__2);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__3 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__3();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__3);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__4 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__4();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__4);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__5 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__5();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__5);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__6 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__6();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__6);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__7 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__7();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__7);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__8 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__8();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__8);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__9 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__9();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__9);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__10 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__10();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__10);
-l___kind_term____x40_Init_System_IO___hyg_2521____closed__11 = _init_l___kind_term____x40_Init_System_IO___hyg_2521____closed__11();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521____closed__11);
-l___kind_term____x40_Init_System_IO___hyg_2521_ = _init_l___kind_term____x40_Init_System_IO___hyg_2521_();
-lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2521_);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__1 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__1();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__1);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__2 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__2();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__2);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__3 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__3();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__3);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__4 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__4();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__4);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__5 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__5();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__5);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__6 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__6();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__6);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__7 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__7();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__7);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__8 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__8();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__8);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__9 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__9();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__9);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__10 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__10();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__10);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__11 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__11();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__11);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__12 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__12();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__12);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__13 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__13();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__13);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__14 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__14();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__14);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__15 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__15();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__15);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__16 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__16();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__16);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__17 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__17();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__17);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__18 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__18();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__18);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__19 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__19();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__19);
-l_myMacro____x40_Init_System_IO___hyg_2569____closed__20 = _init_l_myMacro____x40_Init_System_IO___hyg_2569____closed__20();
-lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2569____closed__20);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__1 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__1();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__1);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__2 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__2();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__2);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__3 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__3();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__3);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__4 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__4();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__4);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__5 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__5();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__5);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__6 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__6();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__6);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__7 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__7();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__7);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__8 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__8();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__8);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__9 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__9();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__9);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__10 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__10();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__10);
+l___kind_term____x40_Init_System_IO___hyg_2535____closed__11 = _init_l___kind_term____x40_Init_System_IO___hyg_2535____closed__11();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535____closed__11);
+l___kind_term____x40_Init_System_IO___hyg_2535_ = _init_l___kind_term____x40_Init_System_IO___hyg_2535_();
+lean_mark_persistent(l___kind_term____x40_Init_System_IO___hyg_2535_);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__1 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__1();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__1);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__2 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__2();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__2);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__3 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__3();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__3);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__4 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__4();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__4);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__5 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__5();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__5);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__6 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__6();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__6);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__7 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__7();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__7);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__8 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__8();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__8);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__9 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__9();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__9);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__10 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__10();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__10);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__11 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__11();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__11);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__12 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__12();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__12);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__13 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__13();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__13);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__14 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__14();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__14);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__15 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__15();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__15);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__16 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__16();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__16);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__17 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__17();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__17);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__18 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__18();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__18);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__19 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__19();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__19);
+l_myMacro____x40_Init_System_IO___hyg_2583____closed__20 = _init_l_myMacro____x40_Init_System_IO___hyg_2583____closed__20();
+lean_mark_persistent(l_myMacro____x40_Init_System_IO___hyg_2583____closed__20);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean
-// Imports: Init Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.Delaborator Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId
+// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.Delaborator Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -14,6 +14,7 @@
 extern "C" {
 #endif
 lean_object* initialize_Init(lean_object*);
+lean_object* initialize_Lean_Data(lean_object*);
 lean_object* initialize_Lean_Compiler(lean_object*);
 lean_object* initialize_Lean_Environment(lean_object*);
 lean_object* initialize_Lean_Modifiers(lean_object*);
@@ -36,6 +37,7 @@ lean_object* initialize_Lean_Delaborator(lean_object*);
 lean_object* initialize_Lean_PrettyPrinter(lean_object*);
 lean_object* initialize_Lean_CoreM(lean_object*);
 lean_object* initialize_Lean_InternalExceptionId(lean_object*);
+lean_object* initialize_Lean_Server(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Lean(lean_object* w) {
 lean_object * res;
@@ -44,6 +46,9 @@ _G_initialized = true;
 res = initialize_Init(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Data(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Lean_Compiler(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -110,6 +115,9 @@ lean_dec_ref(res);
 res = initialize_Lean_InternalExceptionId(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Server(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/Lean/Compiler/InitAttr.c

@@ -64,7 +64,6 @@ uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Lean_registerParametricAttribute___at_Lean_registerInitAttrUnsafe___spec__8___lambda__1___boxed(lean_object*);
 lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_getIOTypeArg___boxed(lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
-extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
 extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__2;
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_InitAttr_0__Lean_isUnitType_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -97,7 +96,6 @@ lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__10;
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_isIOUnitInitFnCore_match__1(lean_object*);
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__14;
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__5;
 lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_507____closed__2;
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__7;
@@ -106,6 +104,7 @@ lean_object* l_Lean_getInitFnNameForCore_x3f___boxed(lean_object*, lean_object*,
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__3(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_isIOUnitBuiltinInitFn___boxed(lean_object*, lean_object*);
+extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 lean_object* l_Std_RBNode_fold___at_Lean_registerInitAttrUnsafe___spec__9___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_registerInitAttrUnsafe___closed__1;
 lean_object* lean_eval_const(lean_object*, lean_object*, lean_object*);
@@ -122,6 +121,7 @@ lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSynta
 lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*);
 extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
 lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 lean_object* l_Lean_registerInitAttrUnsafe___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerInitAttrUnsafe_match__1(lean_object*);
 lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -226,7 +226,7 @@ x_11 = lean_ctor_get(x_5, 1);
 lean_inc(x_11);
 x_12 = lean_ctor_get_usize(x_5, 2);
 lean_dec(x_5);
-x_13 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_13 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_14 = lean_string_dec_eq(x_11, x_13);
 lean_dec(x_11);
 if (x_14 == 0)
@@ -317,7 +317,7 @@ if (lean_obj_tag(x_4) == 0)
 lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; 
 x_5 = lean_ctor_get(x_1, 1);
 x_6 = lean_ctor_get(x_3, 1);
-x_7 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__3;
+x_7 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__3;
 x_8 = lean_string_dec_eq(x_6, x_7);
 if (x_8 == 0)
 {
@@ -395,7 +395,7 @@ x_8 = lean_ctor_get(x_4, 1);
 lean_inc(x_8);
 x_9 = lean_ctor_get_usize(x_4, 2);
 lean_dec(x_4);
-x_10 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+x_10 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 x_11 = lean_string_dec_eq(x_8, x_10);
 lean_dec(x_8);
 if (x_11 == 0)
@@ -468,7 +468,7 @@ if (lean_obj_tag(x_3) == 0)
 {
 lean_object* x_4; lean_object* x_5; uint8_t x_6; 
 x_4 = lean_ctor_get(x_2, 1);
-x_5 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__13;
+x_5 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__13;
 x_6 = lean_string_dec_eq(x_4, x_5);
 return x_6;
 }

stage0/stdlib/Lean/Data.c

@@ -0,0 +1,89 @@
+// Lean compiler output
+// Module: Lean.Data
+// Imports: Init Lean.Data.Format Lean.Data.FormatMacro Lean.Data.Json Lean.Data.JsonRpc Lean.Data.KVMap Lean.Data.LBool Lean.Data.LOption Lean.Data.Lsp Lean.Data.Name Lean.Data.Occurrences Lean.Data.OpenDecl Lean.Data.Options Lean.Data.Position Lean.Data.SMap Lean.Data.Trie
+#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*);
+lean_object* initialize_Lean_Data_Format(lean_object*);
+lean_object* initialize_Lean_Data_FormatMacro(lean_object*);
+lean_object* initialize_Lean_Data_Json(lean_object*);
+lean_object* initialize_Lean_Data_JsonRpc(lean_object*);
+lean_object* initialize_Lean_Data_KVMap(lean_object*);
+lean_object* initialize_Lean_Data_LBool(lean_object*);
+lean_object* initialize_Lean_Data_LOption(lean_object*);
+lean_object* initialize_Lean_Data_Lsp(lean_object*);
+lean_object* initialize_Lean_Data_Name(lean_object*);
+lean_object* initialize_Lean_Data_Occurrences(lean_object*);
+lean_object* initialize_Lean_Data_OpenDecl(lean_object*);
+lean_object* initialize_Lean_Data_Options(lean_object*);
+lean_object* initialize_Lean_Data_Position(lean_object*);
+lean_object* initialize_Lean_Data_SMap(lean_object*);
+lean_object* initialize_Lean_Data_Trie(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Lean_Data(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);
+res = initialize_Lean_Data_Format(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_FormatMacro(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Json(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_JsonRpc(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_KVMap(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_LBool(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_LOption(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Lsp(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Name(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Occurrences(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_OpenDecl(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Options(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Position(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_SMap(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Data_Trie(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

stage0/stdlib/Lean/Data/Format.c

@@ -72,6 +72,7 @@ lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_formatKVMap___closed__1;
 lean_object* l___private_Lean_Data_Format_0__Lean_Format_spaceUptoLine_match__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Data_Format_0__Lean_Format_spaceUptoLine_x27(lean_object*, lean_object*);
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 lean_object* l_Lean_Format_isNil_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_formatEntry_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_String_splitOn(lean_object*, lean_object*);
@@ -275,7 +276,6 @@ lean_object* l_Lean_Format_prefixJoin___rarg(lean_object*, lean_object*, lean_ob
 lean_object* l_Lean_instToFormatProdNameDataValue;
 lean_object* l_Lean_instToFormatArray(lean_object*);
 lean_object* lean_usize_to_nat(size_t);
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_Format_sbracket(lean_object*);
 lean_object* l___private_Lean_Data_Format_0__Lean_Format_spaceUptoLine_x27_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Data_Format_0__Lean_Format_be_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -4339,7 +4339,7 @@ static lean_object* _init_l_Lean_instToFormatFormat() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 return x_1;
 }
 }

stage0/stdlib/Lean/Data/Json/FromToJson.c

@@ -31,6 +31,7 @@ lean_object* l_Lean_instFromJsonString___closed__1;
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_instFromJsonBool___closed__1;
 lean_object* l_Lean_Json_instToJsonStructured_match__1(lean_object*);
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 lean_object* l_Lean_instFromJsonArray_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Json_opt(lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at_Lean_instToJsonArray___spec__1___rarg(lean_object*, size_t, size_t, lean_object*);
@@ -67,7 +68,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_instToJsonArray___spec__1(lean_obj
 lean_object* l_Array_mapMUnsafe_map___at_Lean_instToJsonArray___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instFromJsonArray_match__1(lean_object*);
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_Json_getObjVal_x3f(lean_object*, lean_object*);
 lean_object* l_Lean_Json_getObjValAs_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Json_instFromJsonStructured(lean_object*);
@@ -85,7 +85,7 @@ static lean_object* _init_l_Lean_instToJsonJson() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 return x_1;
 }
 }

stage0/stdlib/Lean/Elab/BuiltinNotation.c

@@ -536,6 +536,7 @@ lean_object* l_Lean_Elab_Term_expandSorry___rarg___closed__4;
 lean_object* l_Lean_Elab_Term_expandInfix___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_hasCDot_match__1(lean_object*);
 lean_object* l_Lean_Elab_Term_elabStateRefT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__20;
 lean_object* l_Lean_Elab_Term_mkPairs_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__8;
 lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_elabSubst___spec__3___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -549,7 +550,6 @@ lean_object* l_Lean_Elab_Term_expandSorry___rarg___closed__1;
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l_Lean_Elab_Term_expandAssert___closed__3;
 lean_object* l___regBuiltin_Lean_Elab_Term_expandUnreachable(lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__20;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_5739____closed__13;
 lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__4;
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_11379____closed__2;
@@ -8625,7 +8625,7 @@ lean_ctor_set(x_64, 2, x_60);
 lean_ctor_set(x_64, 3, x_63);
 x_65 = l_Array_empty___closed__1;
 x_66 = lean_array_push(x_65, x_64);
-x_67 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__20;
+x_67 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__20;
 x_68 = lean_array_push(x_67, x_5);
 x_69 = l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____closed__6;
 x_70 = lean_alloc_ctor(1, 2, 0);

stage0/stdlib/Lean/Elab/Declaration.c

@@ -64,6 +64,7 @@ extern lean_object* l_Array_empty___closed__1;
 lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView_match__3___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabAxiom_match__3(lean_object*);
 lean_object* l_Lean_Elab_Command_elabDeclaration_match__1___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
 lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualPreambleCommand___boxed(lean_object*);
@@ -79,13 +80,13 @@ lean_object* l_Lean_Elab_Command_expandInitCmd___closed__14;
 lean_object* l_Lean_Elab_Command_expandMutualPreamble_match__1(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_expandInitialize(lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_elabDeclaration(lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
 lean_object* l_Lean_Elab_Command_elabAxiom_match__5___rarg(lean_object*, lean_object*);
 lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_elabMutualInductive___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__3(lean_object*);
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__22;
 lean_object* l_List_map___at_Lean_resolveGlobalConst___spec__2(lean_object*);
@@ -129,6 +130,7 @@ lean_object* l_Lean_Elab_Command_expandBuiltinInitialize___boxed(lean_object*, l
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2___closed__2;
 lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__2___rarg(lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__18;
 lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualDef___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1___closed__2;
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3___rarg(lean_object*, lean_object*, lean_object*);
@@ -138,9 +140,9 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMutualPreamble_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView_match__2(lean_object*);
 lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
 lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabAttr___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabAxiom(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__15;
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2___closed__3;
 extern lean_object* l_Lean_Elab_Command_isDefLike___closed__2;
 lean_object* l_Lean_Elab_Command_expandMutualNamespace___closed__1;
@@ -230,14 +232,12 @@ lean_object* l_Lean_Elab_Command_expandMutualElement(lean_object*, lean_object*,
 lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualElement(lean_object*);
 lean_object* l_Lean_Elab_Term_resetMessageLog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__2;
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__15;
 lean_object* l_Lean_Elab_Command_expandInitCmd(uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___regBuiltin_Lean_Elab_Command_elabCheck___closed__1;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1___closed__1;
 extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__27;
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__1;
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__18;
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__4;
 extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__11;
@@ -273,6 +273,7 @@ lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyn
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__13;
 extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3385____closed__10;
 lean_object* l_Lean_Elab_Command_elabMutual___closed__3;
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_object* l_Array_ofSubarray___rarg(lean_object*);
 lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__3;
@@ -308,7 +309,6 @@ lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualNamespace___closed__1;
 lean_object* l_Lean_Elab_Command_elabAxiom_match__5(lean_object*);
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__3;
 lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
 uint8_t l_Lean_Elab_Modifiers_isPrivate(lean_object*);
 lean_object* l_Lean_Elab_Command_elabDeclaration_match__1(lean_object*);
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__9;
@@ -6657,7 +6657,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
@@ -6878,9 +6878,9 @@ lean_ctor_set(x_29, 0, x_28);
 lean_ctor_set(x_29, 1, x_27);
 x_30 = l_Lean_Elab_Command_expandInitCmd___closed__11;
 x_31 = lean_array_push(x_30, x_29);
-x_32 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_32 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 x_33 = l_Lean_addMacroScope(x_17, x_32, x_16);
-x_34 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
+x_34 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
 x_35 = l_Lean_Elab_Command_expandInitCmd___closed__19;
 x_36 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_36, 0, x_21);
@@ -7071,11 +7071,11 @@ lean_ctor_set(x_148, 0, x_147);
 lean_ctor_set(x_148, 1, x_146);
 x_149 = l_Lean_Elab_Command_expandInitCmd___closed__11;
 x_150 = lean_array_push(x_149, x_148);
-x_151 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_151 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_inc(x_111);
 lean_inc(x_112);
 x_152 = l_Lean_addMacroScope(x_112, x_151, x_111);
-x_153 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__10;
+x_153 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__10;
 x_154 = l_Lean_Elab_Command_expandInitCmd___closed__19;
 x_155 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_155, 0, x_142);
@@ -7083,10 +7083,10 @@ lean_ctor_set(x_155, 1, x_153);
 lean_ctor_set(x_155, 2, x_152);
 lean_ctor_set(x_155, 3, x_154);
 x_156 = lean_array_push(x_113, x_155);
-x_157 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_157 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_158 = l_Lean_addMacroScope(x_112, x_157, x_111);
-x_159 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__15;
-x_160 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__18;
+x_159 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__15;
+x_160 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__18;
 x_161 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_161, 0, x_142);
 lean_ctor_set(x_161, 1, x_159);

stage0/stdlib/Lean/Elab/Match.c

@@ -236,6 +236,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___clos
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_8168____closed__8;
 lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_instInhabitedContext;
 lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit___closed__1;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_finalizePatternDecls___spec__2___closed__3;
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -333,6 +334,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabMatch(lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_CollectPatternVars_collect___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabMatch_match__13(lean_object*);
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_strLitKind;
@@ -612,7 +614,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_CollectPatternVars_main_
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_getPatternsVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__5___closed__1;
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
-lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3;
 lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_Result_format___spec__1(lean_object*);
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -870,7 +871,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_ge
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_11379____closed__6;
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_collectPatternVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__1;
-lean_object* l_Lean_Meta_Match_Pattern_toExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabMatch_match__23___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_mkLit(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__1;
@@ -4500,22 +4500,14 @@ return x_10;
 static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("inaccessible");
-return x_1;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_myMacro____x40_Init_Notation___hyg_38____closed__6;
-x_2 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
+x_2 = l_Lean_Meta_Match_Pattern_toExpr_visit___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3() {
+static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2() {
 _start:
 {
 lean_object* x_1; 
@@ -4528,8 +4520,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_Term_termElabAttribute;
-x_3 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
-x_4 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3;
+x_3 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
+x_4 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -9776,7 +9768,7 @@ x_42 = lean_name_eq(x_10, x_41);
 if (x_42 == 0)
 {
 lean_object* x_43; uint8_t x_44; 
-x_43 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
+x_43 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
 x_44 = lean_name_eq(x_10, x_43);
 if (x_44 == 0)
 {
@@ -11176,7 +11168,7 @@ x_382 = lean_name_eq(x_10, x_381);
 if (x_382 == 0)
 {
 lean_object* x_383; uint8_t x_384; 
-x_383 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
+x_383 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
 x_384 = lean_name_eq(x_10, x_383);
 if (x_384 == 0)
 {
@@ -12113,7 +12105,7 @@ x_578 = lean_name_eq(x_10, x_577);
 if (x_578 == 0)
 {
 lean_object* x_579; uint8_t x_580; 
-x_579 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
+x_579 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
 x_580 = lean_name_eq(x_10, x_579);
 if (x_580 == 0)
 {
@@ -13081,7 +13073,7 @@ x_788 = lean_name_eq(x_10, x_787);
 if (x_788 == 0)
 {
 lean_object* x_789; uint8_t x_790; 
-x_789 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
+x_789 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
 x_790 = lean_name_eq(x_10, x_789);
 if (x_790 == 0)
 {
@@ -14112,7 +14104,7 @@ x_1008 = lean_name_eq(x_10, x_1007);
 if (x_1008 == 0)
 {
 lean_object* x_1009; uint8_t x_1010; 
-x_1009 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
+x_1009 = l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1;
 x_1010 = lean_name_eq(x_10, x_1009);
 if (x_1010 == 0)
 {
@@ -23779,9 +23771,10 @@ return x_36;
 lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__5___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
-lean_object* x_9; 
-x_9 = l_Lean_Meta_Match_Pattern_toExpr(x_1, x_4, x_5, x_6, x_7, x_8);
-return x_9;
+uint8_t x_9; lean_object* x_10; 
+x_9 = 0;
+x_10 = l_Lean_Meta_Match_Pattern_toExpr_visit(x_9, x_1, x_4, x_5, x_6, x_7, x_8);
+return x_10;
 }
 }
 static lean_object* _init_l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__5___lambda__2___closed__1() {
@@ -30471,8 +30464,6 @@ l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1 = _init_l___regBuilti
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__1);
 l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2);
-l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3();
-lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__3);
 res = l___regBuiltin_Lean_Elab_Term_elabInaccessible(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);

stage0/stdlib/Lean/Elab/Tactic/Induction.c

@@ -31,7 +31,7 @@ lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
 lean_object* lean_erase_macro_scopes(lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkCasesResult_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438_(lean_object*);
+lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446_(lean_object*);
 lean_object* l_Lean_stringToMessageData(lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
@@ -371,7 +371,6 @@ lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Elab_Tactic_evalInduction___
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalCasesUsing___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalCasesUsing___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
 lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forIn_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfoDefault___spec__1___closed__1;
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -423,6 +422,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_elabTargets___spec__1_
 lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo_match__5(lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecFromUsingLoop_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
 extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo_match__2___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
@@ -441,11 +441,11 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l_Lean_mkApp(lean_object*, lean_object*);
 lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_getRecFromUsing___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Meta_Tactic_Induction_0__Lean_Meta_addRecParams___closed__1;
+lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName(lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_processResult___closed__5;
 lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___closed__2;
-lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts___boxed(lean_object*);
 lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_ElimApp_evalAlts___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfoDefault___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
@@ -8296,21 +8296,31 @@ return x_12;
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_2 = lean_unsigned_to_nat(1u);
-x_3 = l_Lean_Syntax_getArg(x_1, x_2);
-x_4 = l_Lean_Syntax_getSepArgs(x_3);
-lean_dec(x_3);
-return x_4;
-}
-}
-lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts___boxed(lean_object* x_1) {
-_start:
+lean_object* x_2; lean_object* x_3; uint8_t x_4; 
+lean_inc(x_1);
+x_2 = l_Lean_Syntax_getNumArgs(x_1);
+x_3 = lean_unsigned_to_nat(2u);
+x_4 = lean_nat_dec_eq(x_2, x_3);
+lean_dec(x_2);
+if (x_4 == 0)
 {
-lean_object* x_2; 
-x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_1);
+lean_object* x_5; lean_object* x_6; 
+x_5 = l_Lean_Syntax_getArg(x_1, x_3);
 lean_dec(x_1);
-return x_2;
+x_6 = l_Lean_Syntax_getSepArgs(x_5);
+lean_dec(x_5);
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = lean_unsigned_to_nat(1u);
+x_8 = l_Lean_Syntax_getArg(x_1, x_7);
+lean_dec(x_1);
+x_9 = l_Lean_Syntax_getSepArgs(x_8);
+lean_dec(x_8);
+return x_9;
+}
 }
 }
 lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfOptInductionAlts(lean_object* x_1) {
@@ -8324,7 +8334,6 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5;
 x_3 = lean_unsigned_to_nat(0u);
 x_4 = l_Lean_Syntax_getArg(x_1, x_3);
 x_5 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_4);
-lean_dec(x_4);
 return x_5;
 }
 else
@@ -8653,7 +8662,6 @@ lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; size
 x_12 = lean_unsigned_to_nat(0u);
 x_13 = l_Lean_Syntax_getArg(x_1, x_12);
 x_14 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_13);
-lean_dec(x_13);
 x_15 = lean_array_get_size(x_14);
 x_16 = lean_usize_of_nat(x_15);
 lean_dec(x_15);
@@ -11908,7 +11916,6 @@ lean_dec(x_15);
 x_23 = lean_unsigned_to_nat(0u);
 x_24 = l_Lean_Syntax_getArg(x_2, x_23);
 x_25 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_24);
-lean_dec(x_24);
 lean_inc(x_10);
 x_26 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames(x_25, x_22, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_16);
 if (lean_obj_tag(x_26) == 0)
@@ -12114,7 +12121,6 @@ lean_dec(x_60);
 x_68 = lean_unsigned_to_nat(0u);
 x_69 = l_Lean_Syntax_getArg(x_2, x_68);
 x_70 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_69);
-lean_dec(x_69);
 lean_inc(x_10);
 x_71 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames(x_70, x_67, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_61);
 if (lean_obj_tag(x_71) == 0)
@@ -13221,7 +13227,6 @@ lean_free_object(x_18);
 x_24 = lean_unsigned_to_nat(0u);
 x_25 = l_Lean_Syntax_getArg(x_3, x_24);
 x_26 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_25);
-lean_dec(x_25);
 x_27 = l_Lean_Elab_Tactic_getMainGoal(x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_21);
 if (lean_obj_tag(x_27) == 0)
 {
@@ -13482,7 +13487,6 @@ lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
 x_77 = lean_unsigned_to_nat(0u);
 x_78 = l_Lean_Syntax_getArg(x_3, x_77);
 x_79 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_78);
-lean_dec(x_78);
 x_80 = l_Lean_Elab_Tactic_getMainGoal(x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_74);
 if (lean_obj_tag(x_80) == 0)
 {
@@ -17277,7 +17281,7 @@ x_15 = l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_elabTargets___spec__1(x_13,
 return x_15;
 }
 }
-static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1() {
+static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -17287,11 +17291,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
+x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
@@ -17726,7 +17730,7 @@ lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113;
 x_110 = lean_ctor_get(x_105, 1);
 lean_inc(x_110);
 lean_dec(x_105);
-x_111 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
+x_111 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 x_112 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__3(x_111, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_110);
 x_113 = lean_ctor_get(x_112, 0);
 lean_inc(x_113);
@@ -17851,7 +17855,7 @@ x_66 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
 x_67 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_67, 0, x_65);
 lean_ctor_set(x_67, 1, x_66);
-x_68 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
+x_68 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 x_69 = l_Lean_addTrace___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__2(x_68, x_67, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_58);
 x_70 = lean_ctor_get(x_69, 1);
 lean_inc(x_70);
@@ -17887,7 +17891,7 @@ lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean
 x_78 = lean_ctor_get(x_73, 1);
 lean_inc(x_78);
 lean_dec(x_73);
-x_79 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
+x_79 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 x_80 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__3(x_79, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_78);
 x_81 = lean_ctor_get(x_80, 0);
 lean_inc(x_81);
@@ -17937,7 +17941,7 @@ x_99 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
 x_100 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_100, 0, x_98);
 lean_ctor_set(x_100, 1, x_99);
-x_101 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1;
+x_101 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1;
 x_102 = l_Lean_addTrace___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__2(x_101, x_100, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_86);
 x_103 = lean_ctor_get(x_102, 1);
 lean_inc(x_103);
@@ -19198,9 +19202,9 @@ l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTaggedTerm___lamb
 lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTaggedTerm___lambda__1___closed__3);
 l_Lean_Elab_Tactic_elabTargets___boxed__const__1 = _init_l_Lean_Elab_Tactic_elabTargets___boxed__const__1();
 lean_mark_persistent(l_Lean_Elab_Tactic_elabTargets___boxed__const__1);
-l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1();
-lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438____closed__1);
-res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4438_(lean_io_mk_world());
+l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1();
+lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446____closed__1);
+res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_4446_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_Elab_Tactic_evalCasesOn___closed__1 = _init_l_Lean_Elab_Tactic_evalCasesOn___closed__1();

stage0/stdlib/Lean/Exception.c

@@ -87,6 +87,7 @@ lean_object* l_Lean_throwError_match__1(lean_object*);
 lean_object* l_Lean___kind_term____x40_Lean_Exception___hyg_643____closed__5;
 lean_object* l_Lean_myMacro____x40_Lean_Exception___hyg_698____closed__4;
 lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
+extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 lean_object* l_Lean_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instMonadRecDepthReaderT(lean_object*, lean_object*);
 lean_object* l_Lean_Exception_toMessageData_match__1(lean_object*);
@@ -101,7 +102,6 @@ lean_object* l_Lean_myMacro____x40_Lean_Exception___hyg_698____closed__1;
 lean_object* l_Lean___kind_term____x40_Lean_Exception___hyg_643____closed__3;
 lean_object* l_Lean_throwError(lean_object*);
 lean_object* l_Lean_instInhabitedException;
-extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
 lean_object* l_Lean_myMacro____x40_Lean_Exception___hyg_698____closed__2;
 lean_object* l_Lean_withIncRecDepth(lean_object*);
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
@@ -931,7 +931,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
 x_2 = l_Lean___kind_term____x40_Lean_Exception___hyg_595____closed__6;
-x_3 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
+x_3 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -1009,7 +1009,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
 x_2 = l_Lean___kind_term____x40_Lean_Exception___hyg_643____closed__4;
-x_3 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
+x_3 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);

stage0/stdlib/Lean/Expr.c

@@ -169,6 +169,7 @@ lean_object* l_Lean_Expr_isLet_match__1(lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* lean_expr_lift_loose_bvars(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 uint8_t lean_expr_has_level_mvar(lean_object*);
 lean_object* l_Lean_Expr_updateProj_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ExprStructEq_instBEqExprStructEq___closed__1;
@@ -668,7 +669,6 @@ lean_object* l_Lean_Expr_mkData___boxed(lean_object*, lean_object*, lean_object*
 lean_object* l_Lean_ExprStructEq_instToStringExprStructEq(lean_object*);
 lean_object* l_Lean_Expr_isProp_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_BinderInfo_isExplicit___boxed(lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
 uint64_t l_Lean_Expr_mkData___closed__1;
 lean_object* l_List_foldr___at_Lean_mkConst___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_hashEx___boxed(lean_object*);
@@ -5471,7 +5471,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_3 = l_Lean_mkConst(x_2, x_1);
 return x_3;
 }

stage0/stdlib/Lean/KeyedDeclsAttribute.c

@@ -67,6 +67,7 @@ lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 lean_object* l_Std_HashMapImp_find_x3f___at_Lean_KeyedDeclsAttribute_getValues___spec__7___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at_Lean_registerTagAttribute___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_AssocList_find_x3f___at_Lean_KeyedDeclsAttribute_Table_insert___spec__8___rarg(lean_object*, lean_object*);
@@ -112,7 +113,6 @@ lean_object* l___private_Lean_KeyedDeclsAttribute_0__Lean_KeyedDeclsAttribute_mk
 lean_object* l_Lean_KeyedDeclsAttribute_Def_evalKey___default___rarg___closed__1;
 extern lean_object* l_Std_PersistentHashMap_insertAux___rarg___closed__3;
 lean_object* l_Lean_KeyedDeclsAttribute_ExtensionState_table___default___closed__1;
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
 lean_object* l___private_Lean_KeyedDeclsAttribute_0__Lean_KeyedDeclsAttribute_addImported_match__1(lean_object*, lean_object*);
 lean_object* l_Std_mkHashMap___at_Lean_KeyedDeclsAttribute_init___spec__1___rarg(lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_declareBuiltin___rarg___closed__6;
@@ -235,6 +235,7 @@ extern lean_object* l_Lean_regularInitAttr;
 lean_object* l_Lean_KeyedDeclsAttribute_init_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedPersistentEnvExtension___closed__5;
 lean_object* l_Lean_KeyedDeclsAttribute_declareBuiltin___rarg___closed__11;
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 lean_object* l_Lean_SMap_find_x3f___at_Lean_KeyedDeclsAttribute_getValues___spec__1(lean_object*);
 lean_object* lean_nat_mul(lean_object*, lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -265,7 +266,6 @@ lean_object* l_Std_HashMapImp_moveEntries___at_Lean_KeyedDeclsAttribute_Table_in
 lean_object* l_Std_PersistentHashMap_findAux___at_Lean_KeyedDeclsAttribute_Table_insert___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_instInhabitedExtensionState___closed__3;
 lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
 lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_KeyedDeclsAttribute_Table_insert___spec__11___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_KeyedDeclsAttribute_Table_insert___spec__2___rarg___boxed(lean_object*, lean_object*);
@@ -3866,7 +3866,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__4;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__4;
 x_3 = l_Lean_mkConst(x_2, x_1);
 return x_3;
 }
@@ -3876,7 +3876,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_2 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_3 = l_Lean_mkConst(x_2, x_1);
 return x_3;
 }

stage0/stdlib/Lean/Message.c

@@ -97,6 +97,7 @@ lean_object* l_Lean_MessageData_instCoeArrayExprMessageData___boxed(lean_object*
 extern lean_object* l_Lean_formatKVMap___closed__1;
 lean_object* l_Lean_KernelException_toMessageData_match__2(lean_object*);
 extern lean_object* l___kind_term____x40_Init_Notation___hyg_3____closed__1;
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 uint8_t l_Lean_Message_severity___default;
 lean_object* l_Lean_MessageData_instCoeArrayExprMessageData(lean_object*);
 size_t l_USize_shiftRight(size_t, size_t);
@@ -361,7 +362,6 @@ lean_object* lean_message_pos(lean_object*);
 uint8_t l_Lean_MessageLog_isEmpty(lean_object*);
 lean_object* l_Lean_MessageLog_errorsToWarnings_match__1(lean_object*);
 lean_object* l_Lean_KernelException_toMessageData___closed__26;
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_Message_getSeverityEx___boxed(lean_object*);
 lean_object* l_Lean_MessageLog_append___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Message_toString(lean_object*, lean_object*);
@@ -7168,7 +7168,7 @@ static lean_object* _init_l_Lean_instToMessageDataMessageData() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 return x_1;
 }
 }

stage0/stdlib/Lean/Meta/Match.c

@@ -14,13 +14,13 @@
 extern "C" {
 #endif
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux___rarg___closed__2;
+extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__2;
 lean_object* l_Lean_initFn____x40_Lean_Meta_Match___hyg_3_(lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Meta_Match___hyg_3_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAltsAux___rarg___closed__2;
+x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__2;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }

stage0/stdlib/Lean/Parser/Basic.c

@@ -213,6 +213,7 @@ lean_object* l_Lean_Parser_withPosition(lean_object*);
 lean_object* l_Lean_Parser_mkAntiquot___closed__11;
 lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__3___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_updateCache_match__1___rarg(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 lean_object* l_Lean_Parser_charLitFnAux(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_shrink___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_FirstTokens_seq_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -853,7 +854,6 @@ lean_object* l_Lean_Parser_checkWsBefore___elambda__1(lean_object*, lean_object*
 lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*);
 uint8_t l_UInt32_decLe(uint32_t, uint32_t);
 lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__4___rarg(lean_object*, lean_object*);
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_Parser_trailingLoop_match__1___rarg(lean_object*, lean_object*);
 uint8_t l_Lean_Parser_ParserState_hasError(lean_object*);
 lean_object* l_Lean_Parser_symbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -4500,7 +4500,7 @@ static lean_object* _init_l_Lean_Parser_instInhabitedParser___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 x_2 = lean_box(1);
 x_3 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_3, 0, x_1);

stage0/stdlib/Lean/ToExpr.c

@@ -35,8 +35,10 @@ lean_object* l_Lean_instToExprExpr___closed__3;
 lean_object* l_Lean_instToExprProd___rarg___lambda__1___closed__1;
 lean_object* l_Lean_instToExprChar___lambda__1___closed__1;
 extern lean_object* l_Lean_Literal_type___closed__3;
+extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 lean_object* l_Lean_instToExprOption_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instToExprArray(lean_object*);
+extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_6336____closed__5;
 lean_object* l_Lean_instToExprString___closed__1;
 lean_object* l_Lean_instToExprExpr;
@@ -102,7 +104,6 @@ lean_object* l_Lean_instToExprChar___lambda__1(uint32_t);
 lean_object* l_Lean_Name_toExprAux___closed__2;
 lean_object* l_Lean_instToExprChar___lambda__1___boxed(lean_object*);
 lean_object* l_Lean_instToExprProd___rarg___lambda__1___closed__2;
-extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
 extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3385____closed__5;
 lean_object* l_Lean_mkNatLit(lean_object*);
 lean_object* l_Lean_mkStrLit(lean_object*);
@@ -112,7 +113,6 @@ lean_object* l_Lean_instToExprOption_match__1(lean_object*, lean_object*);
 lean_object* l_Lean_instToExprString;
 extern lean_object* l_Lean_Expr_isCharLit___closed__2;
 lean_object* l_Lean_instToExprList(lean_object*);
-extern lean_object* l_instOfNatNat___closed__1;
 lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_List_toExprAux(lean_object*);
 extern lean_object* l_Lean_Expr_isCharLit___closed__4;
@@ -158,7 +158,7 @@ static lean_object* _init_l_Lean_instToExprExpr___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_instOfNatNat___closed__1;
+x_1 = l_Applicative_seqRight___default___rarg___closed__1;
 x_2 = l_Lean_instToExprExpr___closed__3;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -396,7 +396,7 @@ static lean_object* _init_l_Lean_instToExprUnit___lambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_myMacro____x40_Init_System_IO___hyg_2569____closed__16;
+x_1 = l_myMacro____x40_Init_System_IO___hyg_2583____closed__16;
 x_2 = l_Lean_instToExprUnit___lambda__1___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;

stage0/stdlib/Lean/Util/Trace.c

@@ -162,6 +162,7 @@ lean_object* l_Lean_enableTracing(lean_object*);
 lean_object* l_Lean_withNestedTraces___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_PersistentArray_isEmpty___rarg(lean_object*);
 lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_1247____closed__5;
+extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_printTraces___spec__5(lean_object*);
 lean_object* l_Lean_addTrace___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_modifyTraces___rarg___lambda__1(lean_object*, lean_object*);
@@ -178,7 +179,6 @@ size_t l_USize_land(size_t, size_t);
 lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_883____closed__11;
 extern lean_object* l_Lean_nullKind___closed__2;
 extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1881____closed__4;
-extern lean_object* l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
 lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -2922,7 +2922,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l___kind_term____x40_Init_Notation___hyg_3____closed__13;
 x_2 = l_Lean___kind_term____x40_Lean_Util_Trace___hyg_1247____closed__7;
-x_3 = l___kind_term____x40_Init_System_IO___hyg_2521____closed__9;
+x_3 = l___kind_term____x40_Init_System_IO___hyg_2535____closed__9;
 x_4 = lean_alloc_ctor(2, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);