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

@[export lean_is_instance]

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