Helper function for environment extensions and attributes.

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

Equations

• instInhabitedState_mathlib = { default := { state := default, activeScopes := ∅ } }