Helper function for environment extensions and attributes.

@[implicit_reducible]

instance instInhabitedState_mathlib {σ : Type} [Inhabited σ] : Inhabited (Lean.ScopedEnvExtension.State σ)

Equations

• instInhabitedState_mathlib = { default := { state := default } }