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

def Lean.Meta.addGlobalInstance (declName : Lean.Name) (attrKind : Lean.AttributeKind) : Lean.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 : Lean.Environment) (declName : Lean.Name) : Bool

Equations

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