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

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

Equations

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