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.926, ?u.926} Option'.{?u.926}
  [Meta.synthInstance] new goal Functor.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.944, ?u.945}]
  [Meta.synthInstance] ✅ apply @Applicative.toFunctor.{?u.926, ?u.926} to Functor.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Functor.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Functor.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] new goal Applicative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.951,
              ?u.952}, @Alternative.toApplicative.{?u.953, ?u.954}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.926,
          ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Alternative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.926, ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Monad.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
[Meta.synthInstance] ❌ Seq.{?u.926, ?u.926} Option'.{?u.926}
  [Meta.synthInstance] new goal Seq.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.987, ?u.988}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeq.{?u.926, ?u.926} to Seq.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Seq.{?u.926, ?u.926} Option'.{?u.926} ≟ Seq.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] new goal Applicative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.994,
              ?u.995}, @Alternative.toApplicative.{?u.996, ?u.997}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.926,
          ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Alternative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.926, ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Monad.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
[Meta.synthInstance] ❌ SeqLeft.{?u.926, ?u.926} Option'.{?u.926}
  [Meta.synthInstance] new goal SeqLeft.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1012, ?u.1013}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeqLeft.{?u.926, ?u.926} to SeqLeft.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ SeqLeft.{?u.926, ?u.926}
          Option'.{?u.926} ≟ SeqLeft.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] new goal Applicative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1019,
              ?u.1020}, @Alternative.toApplicative.{?u.1021, ?u.1022}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.926,
          ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Alternative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.926, ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Monad.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
[Meta.synthInstance] ❌ SeqRight.{?u.926, ?u.926} Option'.{?u.926}
  [Meta.synthInstance] new goal SeqRight.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1037, ?u.1038}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeqRight.{?u.926, ?u.926} to SeqRight.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ SeqRight.{?u.926, ?u.926}
          Option'.{?u.926} ≟ SeqRight.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] new goal Applicative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1044,
              ?u.1045}, @Alternative.toApplicative.{?u.1046, ?u.1047}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.926,
          ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Alternative.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.926, ?u.926} to Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.926, ?u.926}
          Option'.{?u.926} ≟ Applicative.{?u.926, ?u.926} Option'.{?u.926}
    [Meta.synthInstance] no instances for Monad.{?u.926, ?u.926} Option'.{?u.926}
      [Meta.synthInstance.instances] #[]

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] 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.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance] new goal Functor.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.instances] #[@Applicative.toFunctor.{?u.1502, ?u.1503}]
  [Meta.synthInstance] ✅ apply @Applicative.toFunctor.{?u.1484, ?u.1484} to Functor.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Functor.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Functor.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1509,
              ?u.1510}, @Alternative.toApplicative.{?u.1511, ?u.1512}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] no instances for Alternative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1521}]
  [Meta.synthInstance] ✅ apply instMonadOption'.{?u.1484} to Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Monad.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance.resume] propagating Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 1
  [Meta.synthInstance.resume] propagating Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Functor.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 2
  [Meta.synthInstance] result @Applicative.toFunctor.{?u.1484, ?u.1484} Option'.{?u.1484}
        (@Monad.toApplicative.{?u.1484, ?u.1484} Option'.{?u.1484} instMonadOption'.{?u.1484})
[Meta.synthInstance] ✅ Seq.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance] new goal Seq.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.instances] #[@Applicative.toSeq.{?u.1540, ?u.1541}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeq.{?u.1484, ?u.1484} to Seq.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Seq.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Seq.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1547,
              ?u.1548}, @Alternative.toApplicative.{?u.1549, ?u.1550}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] no instances for Alternative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1557}]
  [Meta.synthInstance] ✅ apply instMonadOption'.{?u.1484} to Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Monad.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance.resume] propagating Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 1
  [Meta.synthInstance.resume] propagating Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Seq.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 2
  [Meta.synthInstance] result @Applicative.toSeq.{?u.1484, ?u.1484} Option'.{?u.1484}
        (@Monad.toApplicative.{?u.1484, ?u.1484} Option'.{?u.1484} instMonadOption'.{?u.1484})
[Meta.synthInstance] ✅ SeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance] new goal SeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.instances] #[@Applicative.toSeqLeft.{?u.1559, ?u.1560}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeqLeft.{?u.1484, ?u.1484} to SeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ SeqLeft.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ SeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1566,
              ?u.1567}, @Alternative.toApplicative.{?u.1568, ?u.1569}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] no instances for Alternative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1576}]
  [Meta.synthInstance] ✅ apply instMonadOption'.{?u.1484} to Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Monad.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance.resume] propagating Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 1
  [Meta.synthInstance.resume] propagating Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} of SeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 2
  [Meta.synthInstance] result @Applicative.toSeqLeft.{?u.1484, ?u.1484} Option'.{?u.1484}
        (@Monad.toApplicative.{?u.1484, ?u.1484} Option'.{?u.1484} instMonadOption'.{?u.1484})
[Meta.synthInstance] ✅ SeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance] new goal SeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.instances] #[@Applicative.toSeqRight.{?u.1578, ?u.1579}]
  [Meta.synthInstance] ✅ apply @Applicative.toSeqRight.{?u.1484,
          ?u.1484} to SeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ SeqRight.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ SeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[@Monad.toApplicative.{?u.1585,
              ?u.1586}, @Alternative.toApplicative.{?u.1587, ?u.1588}]
  [Meta.synthInstance] ✅ apply @Alternative.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] no instances for Alternative.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[]
  [Meta.synthInstance] ✅ apply @Monad.toApplicative.{?u.1484,
          ?u.1484} to Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Applicative.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance] new goal Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
      [Meta.synthInstance.instances] #[instMonadOption'.{?u.1595}]
  [Meta.synthInstance] ✅ apply instMonadOption'.{?u.1484} to Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.tryResolve] ✅ Monad.{?u.1484, ?u.1484}
          Option'.{?u.1484} ≟ Monad.{?u.1484, ?u.1484} Option'.{?u.1484}
  [Meta.synthInstance.resume] propagating Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Monad.{?u.1484, ?u.1484}
        Option'.{?u.1484} of Applicative.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 1
  [Meta.synthInstance.resume] propagating Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} to subgoal Applicative.{?u.1484, ?u.1484}
        Option'.{?u.1484} of SeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
    [Meta.synthInstance.resume] size: 2
  [Meta.synthInstance] result @Applicative.toSeqRight.{?u.1484, ?u.1484} Option'.{?u.1484}
        (@Monad.toApplicative.{?u.1484, ?u.1484} Option'.{?u.1484} instMonadOption'.{?u.1484})


#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) (recFnName : Lean.Name) : Lean.Core.CoreM Lean.Expr 
Lean.Elab.Structural.preprocess: Lean.Expr → 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