import Lean.Elab

structure 
WithLog: Type → Type → Type
WithLog (
logged: Type
logged : 
Type: Type 1
Type) (
α: Type
α : 
Type: Type 1
Type) where
  
log: {logged α : Type} → WithLog logged α → List logged
log : 
List: Type → Type
List 
logged: Type
logged
  
val: {logged α : Type} → WithLog logged α → α
val : 
α: Type
α

instance: {logged : Type} → Monad (WithLog logged)
instance : 
Monad: (Type → Type) → Type 1
Monad <| 
WithLog: Type → Type → Type
WithLog 
logged: Type
logged where
  pure 
val: α✝
val := ⟨
[]: List logged
[], 
val: α✝
val⟩
  bind 
item: WithLog logged α✝
item 
next: α✝ → WithLog logged β✝
next :=
    let rec 
nextItem: {logged α β : Type} → WithLog logged α → (α → WithLog logged β) → WithLog logged β
nextItem := 
next: α✝ → WithLog logged β✝
next 
item: WithLog logged α✝
item.
val: {logged α : Type} → WithLog logged α → α
val
    ⟨
item: WithLog logged α✝
item.
log: {logged α : Type} → WithLog logged α → List logged
log ++ 
nextItem: WithLog logged β✝
nextItem.
log: {logged α : Type} → WithLog logged α → List logged
log, 
nextItem: WithLog logged β✝
nextItem.
val: {logged α : Type} → WithLog logged α → α
val⟩

set_option relaxedAutoImplicit false
set_option autoImplicit false
set_option pp.all true
set_option pp.analyze true
set_option trace.Meta.synthInstance true
set_option synthInstance.checkSynthOrder true

def 
Option': (α : Type u_1) → Type u_1
Option' := 
Option: (α : Type u_1) → Type u_1
Option

-- The error is now gone
-- /--
-- error: fields missing: 'map', 'mapConst', 'seq', 'seqLeft'
-- -/
-- #guard_msgs(error, drop info) in
instance: Monad.{u_1, u_1} Option'.{u_1}
instance : 
Monad: (m : Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
Option': (α : Type u_1) → Type u_1
Option' where
  pure := 
Option.some: {α : Type u_1} → (val : α) → Option.{u_1} α
Option.some
  bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f :=
    let 
b: Option.{u_1} β✝
b := 
Option.bind: {α β : Type u_1} → Option.{u_1} α → (α → Option.{u_1} β) → Option.{u_1} β
Option.bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f
    
b: Option.{u_1} β✝
b
[Meta.synthInstance] ❌️ Functor.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toFunctor.{?u.4, ?u.4} to Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.4, ?u.4} Option'.{?u.4} ≟ Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ Seq.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeq.{?u.4, ?u.4} to Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.4, ?u.4} Option'.{?u.4} ≟ Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeqLeft.{?u.4, ?u.4} to SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.4, ?u.4} Option'.{?u.4} ≟ SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqRight.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeqRight.{?u.4, ?u.4} to SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.4, ?u.4} Option'.{?u.4} ≟ SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>

variable (
logged: Type
logged : 
Type: Type 1
Type) in
#synth 
Monad: (m : Type → Type) → Type 1
Monad <| 
WithLog: (logged α : Type) → Type
WithLog 
logged: Type
logged
@instMonadWithLog logged
[Meta.synthInstance] ✅️ Monad.{0, 0} (WithLog logged)
  [Meta.synthInstance] ✅️ new goal Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.instances] #[@instMonadWithLog]
  [Meta.synthInstance.apply] ✅️ apply @instMonadWithLog to Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.tryResolve] ✅️ Monad.{0, 0} (WithLog logged) ≟ Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.answer] ✅️ Monad.{0, 0} (WithLog logged)
  [Meta.synthInstance] result @instMonadWithLog logged

-- instance : Pure <| WithLog logged where
--   pure val := ⟨[], val⟩

-- -- instance : Bind <| WithLog logged where
-- --   bind item next :=
-- --     let {log := thisLog, .. } := item
-- --     let {log := nextOut, val := nextRes} := next item.val
-- --     ⟨thisLog ++ nextOut, nextRes⟩

-- instance : Bind <| WithLog logged where
--   bind item next :=
--     let nextItem := next item.val
--     ⟨item.log ++ nextItem.log, nextItem.val⟩

-- section CheckInstances

-- variable (logged : Type)

-- /-
-- failed to synthesize
--   Applicative (WithLog logged)
-- -/
-- #synth Applicative <| WithLog logged

-- /-
-- failed to synthesize
--   Monad (WithLog logged)
-- -/
-- #synth Monad <| WithLog logged

-- /-
-- [Meta.synthInstance] ✅ Monad (WithLog logged) ▼
--   [] new goal Monad (WithLog logged) ▶
--   [] ✅ apply @instMonadWithLog to Monad (WithLog logged) ▼
--     [tryResolve] ✅ Monad (WithLog logged) ≟ Monad (WithLog logged)
--   [] result instMonadWithLog
-- -/
-- #synth Monad <| WithLog logged

-- end CheckInstances

-- /-
-- [Meta.synthInstance] ❌ Applicative (WithLog logged) ▶


-- [Meta.synthInstance] ❌ Functor (WithLog logged) ▶


-- [Meta.synthInstance] ✅ Pure (WithLog logged) ▶


-- [Meta.synthInstance] ❌ Seq (WithLog logged) ▶


-- [Meta.synthInstance] ❌ SeqLeft (WithLog logged) ▶


-- [Meta.synthInstance] ❌ SeqRight (WithLog logged) ▶


-- [Meta.synthInstance] ✅ Bind (WithLog logged) ▶
-- -/
-- instance : Monad <| WithLog logged where -- no error

-- variable (logged : Type) in
-- #synth Monad <| WithLog logged

-- def Option' := Option

-- #print Monad.map._default

-- structure A where
--   a : Nat -> Nat := fun x => x

-- structure B extends A where
--   a := A.a._default

/-
@[reducible] def Applicative.map._default.{u_1, u_2} : {f : Type u_1 → Type u_2} →
  Pure.{u_1, u_2} f → Seq.{u_1, u_2} f → {α β : Type u_1} → (α → β) → f α → f β :=
fun {f : Type u_1 → Type u_2} (toPure : Pure.{u_1, u_2} f) (toSeq : Seq.{u_1, u_2} f) =>
  @id.{max (u_1 + 2) (u_2 + 1)} ({α β : Type u_1} → (α → β) → f α → f β) fun {α β : Type u_1} (x : α → β) (y : f α) =>
    @Seq.seq.{u_1, u_2} f toSeq α β (@Pure.pure.{u_1, u_2} f toPure (α → β) x) fun (x : Unit) => y
-/
#print
def Applicative.map._default.{u, v} : {f : Type u → Type v} →
  (pure : {α : Type u} → α → f α) →
    (seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β) → {α β : Type u} → (x : α → β) → (y : f α) → f β :=
fun {f : Type u → Type v} (pure : {α : Type u} → α → f α) (seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β) =>
  @id.{max (u + 2) (v + 1)} ({α β : Type u} → (x : α → β) → (y : f α) → f β) fun {α β : Type u} (x : α → β) (y : f α) =>
    @seq α β (@pure (α → β) x) fun (x : Unit) => y 
Applicative.map._default: {f : Type u → Type v} →
  (pure : {α : Type u} → α → f α) →
    (seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β) → {α β : Type u} → (x : α → β) → (y : f α) → f β
Applicative.map._default

/-
@[reducible] def Monad.map._default.{u_1, u_2} : {m : Type u_1 → Type u_2} →
  Applicative m → Bind m → {α β : Type u_1} → (α → β) → m α → m β :=
fun {m} toApplicative toBind => @id ({α β : Type u_1} → (α → β) → m α → m β) fun {α β} f x => x >>= pure ∘ f
-/
#print
def Monad.map._default.{u, v} : {m : Type u → Type v} →
  (pure : {α : Type u} → α → m α) →
    (bind : {α β : Type u} → m α → (α → m β) → m β) → {α β : Type u} → (f : α → β) → (x : m α) → m β :=
fun {m : Type u → Type v} (pure : {α : Type u} → α → m α) (bind : {α β : Type u} → m α → (α → m β) → m β) =>
  @id.{max (u + 2) (v + 1)} ({α β : Type u} → (f : α → β) → (x : m α) → m β) fun {α β : Type u} (f : α → β) (x : m α) =>
    @bind α β x (@Function.comp.{u + 1, u + 1, v + 1} α β (m β) (@pure β) f) 
Monad.map._default: {m : Type u → Type v} →
  (pure : {α : Type u} → α → m α) →
    (bind : {α β : Type u} → m α → (α → m β) → m β) → {α β : Type u} → (f : α → β) → (x : m α) → m β
Monad.map._default

set_option structureDiamondWarning true

-- instance : Monad Option' where
--   pure := Option.some
--   bind := Option.bind
--   map := Monad.map._default

-- instance : Monad Option' where
--   pure := Option.some
--   bind a f :=
--     let b := Option.bind a f
--     b
--   map f x := Monad.map._default _ _ f x

-- instance : Monad Option' where
--   pure := Option.some
--   bind a f :=
--     let rec b := Option.bind a f
--     b
--   map f x := Monad.map._default _ _ f x

instance: Monad.{u_1, u_1} Option'.{u_1}
instance : 
Monad: (m : Type u_1 → Type u_1) → Type (u_1 + 1)
Monad 
Option': (α : Type u_1) → Type u_1
Option' where
  pure := 
Option.some: {α : Type u_1} → (val : α) → Option.{u_1} α
Option.some
  bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f :=
    let 
c: Option.{u_1} β✝
c :=
      let rec 
b: Option.{u_1} β✝
b := 
Option.bind: {α β : Type u_1} → Option.{u_1} α → (α → Option.{u_1} β) → Option.{u_1} β
Option.bind 
a: Option'.{u_1} α✝
a 
f: α✝ → Option'.{u_1} β✝
f
      
b: Option.{u_1} β✝
b
    
c: Option.{u_1} β✝
c
[Meta.synthInstance] ✅️ Functor.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toFunctor.{?u.4, ?u.4} to Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.4, ?u.4} Option'.{?u.4} ≟ Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.13}]
  [Meta.synthInstance.apply] ✅️ apply instMonadOption'.{?u.4} to Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4} ≟ Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Monad.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Monad.{?u.4, ?u.4} Option'.{?u.4} of Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Applicative.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Applicative.{?u.4, ?u.4} Option'.{?u.4} of Functor.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Functor.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] result @Applicative.toFunctor.{?u.4, ?u.4} Option'.{?u.4}
        (@Monad.toApplicative.{?u.4, ?u.4} Option'.{?u.4} instMonadOption'.{?u.4})
[Meta.synthInstance] ✅️ Seq.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeq.{?u.4, ?u.4} to Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.4, ?u.4} Option'.{?u.4} ≟ Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.13}]
  [Meta.synthInstance.apply] ✅️ apply instMonadOption'.{?u.4} to Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4} ≟ Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Monad.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Monad.{?u.4, ?u.4} Option'.{?u.4} of Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Applicative.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Applicative.{?u.4, ?u.4} Option'.{?u.4} of Seq.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Seq.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] result @Applicative.toSeq.{?u.4, ?u.4} Option'.{?u.4}
        (@Monad.toApplicative.{?u.4, ?u.4} Option'.{?u.4} instMonadOption'.{?u.4})
[Meta.synthInstance] ✅️ SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeqLeft.{?u.4, ?u.4} to SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.4, ?u.4} Option'.{?u.4} ≟ SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.13}]
  [Meta.synthInstance.apply] ✅️ apply instMonadOption'.{?u.4} to Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4} ≟ Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Monad.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Monad.{?u.4, ?u.4} Option'.{?u.4} of Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Applicative.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Applicative.{?u.4, ?u.4} Option'.{?u.4} of SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqLeft.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] result @Applicative.toSeqLeft.{?u.4, ?u.4} Option'.{?u.4}
        (@Monad.toApplicative.{?u.4, ?u.4} Option'.{?u.4} instMonadOption'.{?u.4})
[Meta.synthInstance] ✅️ SeqRight.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] ✅️ new goal SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.7, ?u.8}]
  [Meta.synthInstance.apply] ✅️ apply @Applicative.toSeqRight.{?u.4, ?u.4} to SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.4, ?u.4} Option'.{?u.4} ≟ SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Applicative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.9, ?u.10}, @Alternative.toApplicative.{?u.11, ?u.12}]
  [Meta.synthInstance.apply] ✅️ apply @Alternative.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ no instances for Alternative.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance.apply] ✅️ apply @Monad.toApplicative.{?u.4, ?u.4} to Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4} ≟ Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance] ✅️ new goal Monad.{?u.4, ?u.4} Option'.{?u.4}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.13}]
  [Meta.synthInstance.apply] ✅️ apply instMonadOption'.{?u.4} to Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4} ≟ Monad.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Monad.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Monad.{?u.4, ?u.4} Option'.{?u.4} of Applicative.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance.resume] ✅️ propagating Applicative.{?u.4, ?u.4}
        Option'.{?u.4} to subgoal Applicative.{?u.4, ?u.4} Option'.{?u.4} of SeqRight.{?u.4, ?u.4} Option'.{?u.4}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqRight.{?u.4, ?u.4} Option'.{?u.4}
  [Meta.synthInstance] result @Applicative.toSeqRight.{?u.4, ?u.4} Option'.{?u.4}
        (@Monad.toApplicative.{?u.4, ?u.4} Option'.{?u.4} instMonadOption'.{?u.4})


#check
Lean.Elab.Term.elabLetDecl : Lean.Elab.Term.TermElab 
Lean.Elab.Term.elabLetDecl: Lean.Elab.Term.TermElab
Lean.Elab.Term.elabLetDecl
#check
Lean.Elab.Term.elabLetRec : Lean.Elab.Term.TermElab 
Lean.Elab.Term.elabLetRec: Lean.Elab.Term.TermElab
Lean.Elab.Term.elabLetRec
#check
Lean.Elab.Structural.preprocess (e : Lean.Expr) (recFnNames : Array.{0} Lean.Name) (numFixedParams : Nat) :
  Lean.Core.CoreM Lean.Expr 
Lean.Elab.Structural.preprocess: (e : Lean.Expr) → (recFnNames : Array.{0} Lean.Name) → (numFixedParams : Nat) → Lean.Core.CoreM Lean.Expr
Lean.Elab.Structural.preprocess
#check
Lean.Elab.Command.elabDeclaration : Lean.Elab.Command.CommandElab 
Lean.Elab.Command.elabDeclaration: Lean.Elab.Command.CommandElab
Lean.Elab.Command.elabDeclaration