opaque Lean.Meta.synthInstance.checkSynthOrder : Lean.Option Bool

@[reducible, inline]

abbrev Lean.Meta.InstanceKey : Type

Equations

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

structure Lean.Meta.InstanceEntry : Type

• keys : Array InstanceKey
• val : Expr
• priority : Nat
• globalName? : Option Name
• synthOrder : Array Nat

  The order in which the instance's arguments are to be synthesized.

• attrKind : AttributeKind

instance Lean.Meta.instInhabitedInstanceEntry : Inhabited InstanceEntry

Equations

• Lean.Meta.instInhabitedInstanceEntry = { default := Lean.Meta.instInhabitedInstanceEntry.default }

def Lean.Meta.instInhabitedInstanceEntry.default : InstanceEntry

Equations

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

instance Lean.Meta.instBEqInstanceEntry : BEq InstanceEntry

Equations

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

instance Lean.Meta.instToFormatInstanceEntry : ToFormat InstanceEntry

Equations

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

@[reducible, inline]

abbrev Lean.Meta.InstanceTree : Type

Equations

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

structure Lean.Meta.Instances : Type

• discrTree : InstanceTree
• instanceNames : PHashMap Name InstanceEntry
• erased : PHashSet Name

instance Lean.Meta.instInhabitedInstances : Inhabited Instances

Equations

• Lean.Meta.instInhabitedInstances = { default := Lean.Meta.instInhabitedInstances.default }

def Lean.Meta.instInhabitedInstances.default : Instances

Equations

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

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

Equations

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

def Lean.Meta.Instances.eraseCore (d : Instances) (declName : Name) : 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] [MonadError m] (d : Instances) (declName : Name) : m Instances

Equations

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

opaque Lean.Meta.instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances

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

Equations

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

def Lean.Meta.getGlobalInstancesIndex : CoreM (DiscrTree 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 : CoreM (PHashSet 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 : Environment) (declName : Name) : Bool

Equations

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

def Lean.Meta.isInstance (declName : Name) : 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 : Name) : CoreM (Option Nat)

Equations

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

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

Equations

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

Default instance support

structure Lean.Meta.DefaultInstanceEntry : Type

• className : Name
• instanceName : Name
• priority : Nat

@[reducible, inline]

abbrev Lean.Meta.PrioritySet : Type

Equations

• Lean.Meta.PrioritySet = Std.TreeSet Nat fun (x y : Nat) => compare y x

structure Lean.Meta.DefaultInstances : Type

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

instance Lean.Meta.instInhabitedDefaultInstances : Inhabited DefaultInstances

Equations

• Lean.Meta.instInhabitedDefaultInstances = { default := Lean.Meta.instInhabitedDefaultInstances.default }

def Lean.Meta.instInhabitedDefaultInstances.default : DefaultInstances

Equations

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

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

Equations

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

opaque Lean.Meta.defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances

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

Equations

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

def Lean.Meta.getDefaultInstancesPriorities {m : Type → Type} [Monad m] [MonadEnv m] : m 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] [MonadEnv m] (className : Name) : m (List (Name × Nat))

Equations

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