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

@[reducible, inline]

abbrev Lean.Meta.InstanceKey : Type

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_reducible]

instance Lean.Meta.instInhabitedInstanceEntry : Inhabited InstanceEntry

@[instance_reducible]

instance Lean.Meta.instBEqInstanceEntry : BEq InstanceEntry

@[instance_reducible]

instance Lean.Meta.instToFormatInstanceEntry : ToFormat InstanceEntry

@[reducible, inline]

abbrev Lean.Meta.InstanceTree : Type

structure Lean.Meta.Instances : Type

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

@[instance_reducible]

instance Lean.Meta.instInhabitedInstances : Inhabited Instances

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

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

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

opaque Lean.Meta.instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances

def Lean.Meta.checkImpossibleInstance (cinfo : ConstantInfo) : MetaM Unit

def Lean.Meta.checkNonClassInstance (c : Expr) : MetaM Unit

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

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

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

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

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

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

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

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

Default instance support

structure Lean.Meta.DefaultInstanceEntry : Type

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

@[reducible, inline]

abbrev Lean.Meta.PrioritySet : Type

structure Lean.Meta.DefaultInstances : Type

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

@[instance_reducible]

instance Lean.Meta.instInhabitedDefaultInstances : Inhabited DefaultInstances

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

opaque Lean.Meta.defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances

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

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

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