@[inline]

abbrev Lean.Meta.InstanceKey : Type

Equations

• Lean.Meta.InstanceKey = Lean.Meta.DiscrTree.Key false

structure Lean.Meta.InstanceEntry : Type

• keys : Array Lean.Meta.InstanceKey
• val : Lean.Expr
• priority : Nat
• globalName? : Option Lean.Name
• attrKind : Lean.AttributeKind

instance Lean.Meta.instInhabitedInstanceEntry : Inhabited Lean.Meta.InstanceEntry

Equations

• Lean.Meta.instInhabitedInstanceEntry = { default := { keys := default, val := default, priority := default, globalName? := default, attrKind := default } }

instance Lean.Meta.instBEqInstanceEntry : BEq Lean.Meta.InstanceEntry

Equations

• Lean.Meta.instBEqInstanceEntry = { beq := fun e₁ e₂ => e₁.val == e₂.val }

instance Lean.Meta.instToFormatInstanceEntry : Lean.ToFormat Lean.Meta.InstanceEntry

Equations

• Lean.Meta.instToFormatInstanceEntry = { format := fun e => match e.globalName? with | some n => Std.format n | x => Std.Format.text "<local>" }

@[inline]

abbrev Lean.Meta.InstanceTree : Type

Equations

• Lean.Meta.InstanceTree = Lean.Meta.DiscrTree Lean.Meta.InstanceEntry false

structure Lean.Meta.Instances : Type

• discrTree : Lean.Meta.InstanceTree
• instanceNames : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry
• erased : Lean.PHashSet Lean.Name

instance Lean.Meta.instInhabitedInstances : Inhabited Lean.Meta.Instances

Equations

• Lean.Meta.instInhabitedInstances = { default := { discrTree := default, instanceNames := default, erased := default } }

def Lean.Meta.addInstanceEntry (d : Lean.Meta.Instances) (e : Lean.Meta.InstanceEntry) : Lean.Meta.Instances

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Instances.eraseCore (d : Lean.Meta.Instances) (declName : Lean.Name) : Lean.Meta.Instances

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Instances.erase {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (d : Lean.Meta.Instances) (declName : Lean.Name) : m Lean.Meta.Instances

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.instanceExtension : Lean.SimpleScopedEnvExtension Lean.Meta.InstanceEntry Lean.Meta.Instances

def Lean.Meta.addInstance (declName : Lean.Name) (attrKind : Lean.AttributeKind) (prio : Nat) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.getGlobalInstancesIndex : Lean.CoreM (Lean.Meta.DiscrTree Lean.Meta.InstanceEntry false)

Equations

• Lean.Meta.getGlobalInstancesIndex = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.instanceExtension __do_lift).discrTree

def Lean.Meta.getErasedInstances : Lean.CoreM (Lean.PHashSet Lean.Name)

Equations

• Lean.Meta.getErasedInstances = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.instanceExtension __do_lift).erased

def Lean.Meta.isInstance (declName : Lean.Name) : Lean.CoreM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.getInstancePriority? (declName : Lean.Name) : Lean.CoreM (Option Nat)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.getInstanceAttrKind? (declName : Lean.Name) : Lean.CoreM (Option Lean.AttributeKind)

Equations

• One or more equations did not get rendered due to their size.

Default instance support

structure Lean.Meta.DefaultInstanceEntry : Type

• className : Lean.Name
• instanceName : Lean.Name
• priority : Nat

@[inline]

abbrev Lean.Meta.PrioritySet : Type

Equations

• Lean.Meta.PrioritySet = Lean.RBTree Nat fun x y => compare y x

structure Lean.Meta.DefaultInstances : Type

• defaultInstances : Lean.NameMap (List (Lean.Name × Nat))
• priorities : Lean.Meta.PrioritySet

instance Lean.Meta.instInhabitedDefaultInstances : Inhabited Lean.Meta.DefaultInstances

Equations

• Lean.Meta.instInhabitedDefaultInstances = { default := { defaultInstances := default, priorities := default } }

def Lean.Meta.addDefaultInstanceEntry (d : Lean.Meta.DefaultInstances) (e : Lean.Meta.DefaultInstanceEntry) : Lean.Meta.DefaultInstances

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.defaultInstanceExtension : Lean.SimplePersistentEnvExtension Lean.Meta.DefaultInstanceEntry Lean.Meta.DefaultInstances

def Lean.Meta.addDefaultInstance (declName : Lean.Name) (prio : optParam Nat 0) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.getDefaultInstancesPriorities {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] : m Lean.Meta.PrioritySet

Equations

• Lean.Meta.getDefaultInstancesPriorities = do let __do_lift ← Lean.getEnv pure (Lean.SimplePersistentEnvExtension.getState Lean.Meta.defaultInstanceExtension __do_lift).priorities

def Lean.Meta.getDefaultInstances {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (className : Lean.Name) : m (List (Lean.Name × Nat))

Equations

• One or more equations did not get rendered due to their size.