Documentation
Lean
.
Meta
.
GlobalInstances
Search
return to top
source
Imports
Lean.ScopedEnvExtension
Lean.Meta.Basic
Imported by
Lean
.
Meta
.
globalInstanceExtension
Lean
.
Meta
.
addGlobalInstance
Lean
.
Meta
.
isGlobalInstance
source
opaque
Lean
.
Meta
.
globalInstanceExtension
:
SimpleScopedEnvExtension
Name
(
PersistentHashMap
Name
Unit
)
source
def
Lean
.
Meta
.
addGlobalInstance
(declName :
Name
)
(attrKind :
AttributeKind
)
:
MetaM
Unit
Equations
Lean.Meta.addGlobalInstance
declName
attrKind
=
Lean.ScopedEnvExtension.add
Lean.Meta.globalInstanceExtension
declName
attrKind
Instances For
source
@[export lean_is_instance]
def
Lean
.
Meta
.
isGlobalInstance
(env :
Environment
)
(declName :
Name
)
:
Bool
Equations
Lean.Meta.isGlobalInstance
env
declName
=
(
Lean.ScopedEnvExtension.getState
Lean.Meta.globalInstanceExtension
env
)
.
contains
declName
Instances For