source
opaque Lean.Meta.synthInstance.checkSynthOrder :
Lean.Option Bool
source
@[reducible, inline]
abbrev Lean.Meta.InstanceKey :
Type
Equations

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

Instances For

source
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

Instances For

source
def Lean.Meta.instInhabitedInstanceEntry.default :
InstanceEntry
Equations

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

Instances For

source
instance Lean.Meta.instInhabitedInstanceEntry :
Inhabited InstanceEntry
Equations

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

source
instance Lean.Meta.instBEqInstanceEntry :
BEq InstanceEntry
Equations

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

source
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>" }

source
@[reducible, inline]
abbrev Lean.Meta.InstanceTree :
Type
Equations

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

Instances For

source
structure Lean.Meta.Instances :
Type

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

Instances For

source
def Lean.Meta.instInhabitedInstances.default :
Instances
Equations

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

Instances For

source
instance Lean.Meta.instInhabitedInstances :
Inhabited Instances
Equations

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

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

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

Instances For

source
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 }

Instances For

source
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.

Instances For

source
opaque Lean.Meta.instanceExtension :
SimpleScopedEnvExtension InstanceEntry Instances
source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

# Default instance support #

source
structure Lean.Meta.DefaultInstanceEntry :
Type

- className : Name
- instanceName : Name
- priority : Nat

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.PrioritySet :
Type
Equations

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

Instances For

source
structure Lean.Meta.DefaultInstances :
Type

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

Instances For

source
instance Lean.Meta.instInhabitedDefaultInstances :
Inhabited DefaultInstances
Equations

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

source
def Lean.Meta.instInhabitedDefaultInstances.default :
DefaultInstances
Equations

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

Instances For

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

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

Instances For

source
opaque Lean.Meta.defaultInstanceExtension :
SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances
source
def Lean.Meta.addDefaultInstance (declName : Name) (prio : Nat := 0) :
MetaM Unit
Equations

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

Instances For

source
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

Instances For

source
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 [])

Instances For