@[instance_reducible]

instance Lake.instMonadDStoreStateTDTreeMapOfMonadOfLawfulEqCmp {κ : Type u_1} {m : Type (max u_1 u_2) → Type u_3} {β : κ → Type (max u_2 u_1)} {cmp : κ → κ → Ordering} [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateT (Std.DTreeMap κ β cmp) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadDStoreStateRefT'DTreeMapOfMonadLiftTSTOfMonadOfLawfulEqCmp {κ ω : Type} {m : Type → Type} {β : κ → Type} {cmp : κ → κ → Ordering} [MonadLiftT (ST ω) m] [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateRefT' ω (Std.DTreeMap κ β cmp) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadStoreStateTRBArrayOfMonad {m : Type (max u_1 u_2) → Type u_3} {κ : Type u_1} {α : Type (max u_2 u_1)} {cmp : κ → κ → Ordering} [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadStoreStateRefT'RBArrayOfMonadLiftTSTOfMonad {ω : Type} {m : Type → Type} {κ α : Type} {cmp : κ → κ → Ordering} [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBArray κ α cmp) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadStoreNameStateTNameMapOfMonad {m : Type → Type u_1} {α : Type} [Monad m] : MonadStore Lean.Name α (StateT (Lean.NameMap α) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadStoreNameStateRefT'NameMapOfMonadLiftTSTOfMonad {ω : Type} {m : Type → Type} {α : Type} [MonadLiftT (ST ω) m] [Monad m] : MonadStore Lean.Name α (StateRefT' ω (Lean.NameMap α) m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lake.instMonadStore1OfOfMonadDStoreOfFamilyOut {κ : Type u_1} {β : κ → Type u_2} {m : Type u_2 → Type u_3} {k : κ} {α : Type u_2} [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m

Equations

• Lake.instMonadStore1OfOfMonadDStoreOfFamilyOut = { fetch? := cast ⋯ (Lake.fetch? k), store := fun (a : α) => Lake.store k (cast ⋯ a) }