opaque Lean.Meta.globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit)

def Lean.Meta.addGlobalInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Equations

• Lean.Meta.addGlobalInstance declName attrKind = Lean.ScopedEnvExtension.add Lean.Meta.globalInstanceExtension declName attrKind

@[export lean_is_instance]

def Lean.Meta.isGlobalInstance (env : Environment) (declName : Name) : Bool

Equations

• Lean.Meta.isGlobalInstance env declName = (Lean.ScopedEnvExtension.getState Lean.Meta.globalInstanceExtension env).contains declName