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: 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

error: fields missing: 'map', 'mapConst', 'seq', 'seqLeft'

#guard_msgs
Error: ❌️ Docstring on `#guard_msgs` does not match generated message:

error: fields missing: 'map', 'mapConst', 'seq', 'seqLeft'(error, drop info) in
instance: Monad.{u_1, u_1} Option'.{u_1}
instance : 
Monad: (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} → α → 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
Error: fields missing: 'map', 'mapConst', 'seq', 'seqLeft'
[Meta.synthInstance] ❌️ Functor.{?u.931, ?u.931} Option'.{?u.931}
  [Meta.synthInstance] new goal Functor.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.949, ?u.950}]
  [Meta.synthInstance] ✅️ apply @Applicative.toFunctor.{?u.931, ?u.931} to Functor.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Functor.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] new goal Applicative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.956,
              ?u.957}, @Alternative.toApplicative.{?u.958, ?u.959}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.931,
          ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Alternative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.931, ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Monad.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ Seq.{?u.931, ?u.931} Option'.{?u.931}
  [Meta.synthInstance] new goal Seq.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.992, ?u.993}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeq.{?u.931, ?u.931} to Seq.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.931, ?u.931} Option'.{?u.931} ≟ Seq.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] new goal Applicative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.999,
              ?u.1000}, @Alternative.toApplicative.{?u.1001, ?u.1002}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.931,
          ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Alternative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.931, ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Monad.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqLeft.{?u.931, ?u.931} Option'.{?u.931}
  [Meta.synthInstance] new goal SeqLeft.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1017, ?u.1018}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqLeft.{?u.931, ?u.931} to SeqLeft.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.931, ?u.931}
          Option'.{?u.931} ≟ SeqLeft.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] new goal Applicative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1024,
              ?u.1025}, @Alternative.toApplicative.{?u.1026, ?u.1027}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.931,
          ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Alternative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.931, ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Monad.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ SeqRight.{?u.931, ?u.931} Option'.{?u.931}
  [Meta.synthInstance] new goal SeqRight.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1042, ?u.1043}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqRight.{?u.931, ?u.931} to SeqRight.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.931, ?u.931}
          Option'.{?u.931} ≟ SeqRight.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] new goal Applicative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1049,
              ?u.1050}, @Alternative.toApplicative.{?u.1051, ?u.1052}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.931,
          ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Alternative.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.931, ?u.931} to Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.931, ?u.931}
          Option'.{?u.931} ≟ Applicative.{?u.931, ?u.931} Option'.{?u.931}
    [Meta.synthInstance] no instances for Monad.{?u.931, ?u.931} Option'.{?u.931}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] result <not-available>

variable (
logged: Type
logged : 
Type: Type 1
Type) in
#synth 
Monad: (Type → Type) → Type 1
Monad <| 
WithLog: Type → Type → Type
WithLog 
logged: Type
logged
[Meta.synthInstance] ✅️ Monad.{0, 0} (WithLog logged)
  [Meta.synthInstance] new goal Monad.{0, 0} (WithLog logged)
    [Meta.synthInstance.instances] #[@instMonadWithLog]
  [Meta.synthInstance] ✅️ 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
@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
@[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 
Applicative.map._default: {f : Type u_1 → Type u_2} → Pure.{u_1, u_2} f → Seq.{u_1, u_2} f → {α β : Type u_1} → (α → β) → 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
@[reducible] def Monad.map._default.{u_1, u_2} : {m : Type u_1 → Type u_2} →
  Applicative.{u_1, u_2} m → Bind.{u_1, u_2} m → {α β : Type u_1} → (α → β) → m α → m β :=
fun {m : Type u_1 → Type u_2} (toApplicative : Applicative.{u_1, u_2} m) (toBind : Bind.{u_1, u_2} m) =>
  @id.{max (u_1 + 2) (u_2 + 1)} ({α β : Type u_1} → (α → β) → m α → m β) fun {α β : Type u_1} (f : α → β) (x : m α) =>
    @Bind.bind.{u_1, u_2} m toBind α β x
      (@Function.comp.{u_1 + 1, u_1 + 1, u_2 + 1} α β (m β)
        (@Pure.pure.{u_1, u_2} m (@Applicative.toPure.{u_1, u_2} m toApplicative) β) f) 
Monad.map._default: {m : Type u_1 → Type u_2} → Applicative.{u_1, u_2} m → Bind.{u_1, u_2} m → {α β : Type u_1} → (α → β) → 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: (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} → α → 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.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] new goal Functor.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.1507, ?u.1508}]
  [Meta.synthInstance] ✅️ apply @Applicative.toFunctor.{?u.1489,
          ?u.1489} to Functor.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Functor.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Functor.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1514,
              ?u.1515}, @Alternative.toApplicative.{?u.1516, ?u.1517}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] no instances for Alternative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1526}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1489} to Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Functor.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Functor.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] result @Applicative.toFunctor.{?u.1489, ?u.1489} Option'.{?u.1489}
        (@Monad.toApplicative.{?u.1489, ?u.1489} Option'.{?u.1489} instMonadOption'.{?u.1489})
[Meta.synthInstance] ✅️ Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] new goal Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.1545, ?u.1546}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeq.{?u.1489, ?u.1489} to Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Seq.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1552,
              ?u.1553}, @Alternative.toApplicative.{?u.1554, ?u.1555}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] no instances for Alternative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1562}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1489} to Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ Seq.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] result @Applicative.toSeq.{?u.1489, ?u.1489} Option'.{?u.1489}
        (@Monad.toApplicative.{?u.1489, ?u.1489} Option'.{?u.1489} instMonadOption'.{?u.1489})
[Meta.synthInstance] ✅️ SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] new goal SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1564, ?u.1565}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqLeft.{?u.1489,
          ?u.1489} to SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ SeqLeft.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1571,
              ?u.1572}, @Alternative.toApplicative.{?u.1573, ?u.1574}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] no instances for Alternative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1581}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1489} to Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} of SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] result @Applicative.toSeqLeft.{?u.1489, ?u.1489} Option'.{?u.1489}
        (@Monad.toApplicative.{?u.1489, ?u.1489} Option'.{?u.1489} instMonadOption'.{?u.1489})
[Meta.synthInstance] ✅️ SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] new goal SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1583, ?u.1584}]
  [Meta.synthInstance] ✅️ apply @Applicative.toSeqRight.{?u.1489,
          ?u.1489} to SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ SeqRight.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1590,
              ?u.1591}, @Alternative.toApplicative.{?u.1592, ?u.1593}]
  [Meta.synthInstance] ✅️ apply @Alternative.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] no instances for Alternative.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅️ apply @Monad.toApplicative.{?u.1489,
          ?u.1489} to Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Applicative.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance] new goal Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1600}]
  [Meta.synthInstance] ✅️ apply instMonadOption'.{?u.1489} to Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.tryResolve] ✅️ Monad.{?u.1489, ?u.1489}
          Option'.{?u.1489} ≟ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.answer] ✅️ Monad.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Monad.{?u.1489, ?u.1489}
        Option'.{?u.1489} of Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.answer] ✅️ Applicative.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance.resume] propagating Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} to subgoal Applicative.{?u.1489, ?u.1489}
        Option'.{?u.1489} of SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
    [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.answer] ✅️ SeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
  [Meta.synthInstance] result @Applicative.toSeqRight.{?u.1489, ?u.1489} Option'.{?u.1489}
        (@Monad.toApplicative.{?u.1489, ?u.1489} Option'.{?u.1489} instMonadOption'.{?u.1489})


#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) : Lean.Core.CoreM Lean.Expr 
Lean.Elab.Structural.preprocess: Lean.Expr → Array.{0} Lean.Name → Lean.Core.CoreM Lean.Expr
Lean.Elab.Structural.preprocess
#check
Lean.Elab.Command.elabStructure (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) :
  Lean.Elab.Command.CommandElabM Unit 
Lean.Elab.Command.elabStructure: Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
Lean.Elab.Command.elabStructure