Helper function for environment extensions and attributes.

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

Equations

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