Documentation

Lean.Meta.GlobalInstances

source
opaque Lean.Meta.globalInstanceExtension :
SimpleScopedEnvExtension Name (PersistentHashMap Name Unit)
source
def Lean.Meta.addGlobalInstance (declName : Name) (attrKind : AttributeKind) :
MetaM Unit
Equations
    Instances For
      source
      @[export lean_is_instance]
      def Lean.Meta.isGlobalInstance (env : Environment) (declName : Name) :
      Bool
      Equations
        Instances For