Documentation

Lean.Meta.GlobalInstances

opaque Lean.Meta.globalInstanceExtension:

Lean.SimpleScopedEnvExtension Lean.Name (Std.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) :

Equations

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