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

@[inline, reducible]

abbrev Lean.Meta.InstanceKey : Type

structure Lean.Meta.InstanceEntry : Type

• 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

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

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

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

@[inline, reducible]

abbrev Lean.Meta.InstanceTree : Type

structure Lean.Meta.Instances : Type

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

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

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

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

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

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

def Lean.Meta.computeSynthOrder (inst : Lean.Expr) : Lean.MetaM (Array Nat)

Compute the order the arguments of inst should by synthesized.

The synthesization order makes sure that all mvars in non-out-params of the subgoals are assigned before we try to synthesize it. Otherwise it goes left to right.

For example:

• [Add α] [Zero α] : Foo α returns [0, 1]
• [Mul A] [Mul B] [MulHomClass F A B] : FunLike F A B returns [2, 0, 1] (because A B are out-params and are only filled in once we synthesize 2)

(The type of inst must not contain mvars.)

def Lean.Meta.computeSynthOrder.getSemiOutParamPositionsOf (classTy : Lean.Expr) : Lean.MetaM (Array Nat)

partial def Lean.Meta.computeSynthOrder.assignMVarsIn (argMVars : Array Lean.Expr) (argVars : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM Unit

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

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

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

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

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

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

Default instance support

structure Lean.Meta.DefaultInstanceEntry : Type

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

@[inline, reducible]

abbrev Lean.Meta.PrioritySet : Type

structure Lean.Meta.DefaultInstances : Type

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

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

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

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

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

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