Documentation

Lean.Meta.Instances

opaque Lean.Meta.synthInstance.checkSynthOrder :

Lean.Option Bool

@[reducible, inline]

abbrev Lean.Meta.InstanceKey :

Equations

Lean.Meta.InstanceKey = Lean.Meta.DiscrTree.Key

structure Lean.Meta.InstanceEntry :

keys : Array Lean.Meta.InstanceKey
val : Lean.Expr
priority : Nat
globalName? : Option Lake.Name
synthOrder : Array Nat
The order in which the instance's arguments are to be synthesized.
attrKind : Lean.AttributeKind

Instances For

instance Lean.Meta.instInhabitedInstanceEntry :

Inhabited Lean.Meta.InstanceEntry

Equations

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

instance Lean.Meta.instBEqInstanceEntry :

BEq Lean.Meta.InstanceEntry

Equations

Lean.Meta.instBEqInstanceEntry = { beq := fun (e₁ e₂ : Lean.Meta.InstanceEntry) => e₁.val == e₂.val }

instance Lean.Meta.instToFormatInstanceEntry :

Lean.ToFormat Lean.Meta.InstanceEntry

Equations

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

@[reducible, inline]

abbrev Lean.Meta.InstanceTree :

Equations

Lean.Meta.InstanceTree = Lean.Meta.DiscrTree Lean.Meta.InstanceEntry

structure Lean.Meta.Instances :

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

Instances For

Lean.Meta.instInhabitedInstances

instance Lean.Meta.instInhabitedInstances :

Inhabited Lean.Meta.Instances

Equations

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

def Lean.Meta.tcDtConfig :

Lean.Meta.WhnfCoreConfig

Configuration for the discrimination tree module

Equations

Lean.Meta.tcDtConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

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 : Lake.Name) :

Lean.Meta.Instances

Equations

d.eraseCore declName = { discrTree := d.discrTree, instanceNames := Lean.PersistentHashMap.erase d.instanceNames declName, erased := Lean.PersistentHashSet.insert d.erased declName }

def Lean.Meta.Instances.erase {m : Type → Type} [Monad m] [Lean.MonadError m] (d : Lean.Meta.Instances) (declName : Lake.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 : Lake.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 __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.instanceExtension __do_lift).discrTree

def Lean.Meta.getErasedInstances :

Lean.CoreM (Lean.PHashSet Lake.Name)

Equations

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

def Lean.Meta.isInstanceCore (env : Lean.Environment) (declName : Lake.Name) :

Equations

Lean.Meta.isInstanceCore env declName = Lean.PersistentHashMap.contains (Lean.ScopedEnvExtension.getState Lean.Meta.instanceExtension env).instanceNames declName

def Lean.Meta.isInstance (declName : Lake.Name) :

Lean.CoreM Bool

Equations

Lean.Meta.isInstance declName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.isInstanceCore __do_lift declName)

def Lean.Meta.getInstancePriority? (declName : Lake.Name) :

Lean.CoreM (Option Nat)

Equations

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

def Lean.Meta.getInstanceAttrKind? (declName : Lake.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 :

className : Lake.Name
instanceName : Lake.Name
priority : Nat

@[reducible, inline]

abbrev Lean.Meta.PrioritySet :

Equations

Lean.Meta.PrioritySet = Lean.RBTree Nat fun (x y : Nat) => compare y x

structure Lean.Meta.DefaultInstances :

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

Instances For

Lean.Meta.instInhabitedDefaultInstances

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 : Lake.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} [Monad m] [Lean.MonadEnv m] :

m Lean.Meta.PrioritySet

Equations

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

def Lean.Meta.getDefaultInstances {m : Type → Type} [Monad m] [Lean.MonadEnv m] (className : Lake.Name) :

m (List (Lake.Name × Nat))

Equations

Lean.Meta.getDefaultInstances className = do let __do_lift ← Lean.getEnv pure (((Lean.Meta.defaultInstanceExtension.getState __do_lift).defaultInstances.find? className).getD [])