Documentation

Lean.Meta.Instances

structure Lean.Meta.InstanceEntry:

Type

keys : Array Lean.Meta.DiscrTree.Key
val : Lean.Expr
priority : Nat
globalName? : Option Lean.Name

instance Lean.Meta.instInhabitedInstanceEntry:

Inhabited Lean.Meta.InstanceEntry

Equations

Lean.Meta.instInhabitedInstanceEntry = { default := { keys := default, val := default, priority := default, globalName? := 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 => Lean.format n | x => Std.Format.text "<local>" }

structure Lean.Meta.Instances:

Type

discrTree : Lean.Meta.DiscrTree Lean.Meta.InstanceEntry
instanceNames : Std.PHashSet Lean.Name
erased : Std.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)

Equations

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

def Lean.Meta.getErasedInstances:

Lean.CoreM (Std.PHashSet Lean.Name)

Equations

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

structure Lean.Meta.DefaultInstanceEntry:

Type

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

@[inline]

abbrev Lean.Meta.PrioritySet:

Type

Equations

Lean.Meta.PrioritySet = Std.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 a ← Lean.getEnv pure (Lean.SimplePersistentEnvExtension.getState Lean.Meta.defaultInstanceExtension a).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.