Lean.Meta.Instances

Lean.Meta.addInstanceEntry d e = match e.globalName? with | some n => { discrTree := Lean.Meta.DiscrTree.insertCore d.discrTree e.keys e, instanceNames := Std.PersistentHashSet.insert d.instanceNames n, erased := d.erased } | none => { discrTree := Lean.Meta.DiscrTree.insertCore d.discrTree e.keys e, instanceNames := d.instanceNames, erased := d.erased }

source

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

Lean.Meta.Instances

Equations

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

source

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

m Lean.Meta.Instances

Equations

Lean.Meta.Instances.erase d declName = let _do_jp := fun y => pure (Lean.Meta.Instances.eraseCore d declName); if Std.PersistentHashSet.contains d.instanceNames declName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData declName ++ Lean.toMessageData "' does not have [instance] attribute") _do_jp y

source

constant Lean.Meta.instanceExtension :

Lean.SimpleScopedEnvExtension Lean.Meta.InstanceEntry Lean.Meta.Instances

source

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

Lean.MetaM Unit

Equations

Lean.Meta.addInstance declName attrKind prio = do let c ← Lean.mkConstWithLevelParams declName let keys ← Lean.Meta.mkInstanceKey c Lean.Meta.addGlobalInstance declName attrKind Lean.ScopedEnvExtension.add Lean.Meta.instanceExtension { keys := keys, val := c, priority := prio, globalName? := some declName } attrKind

source

def Lean.Meta.getGlobalInstancesIndex :

Lean.CoreM (Lean.Meta.DiscrTree Lean.Meta.InstanceEntry)

Equations

Lean.Meta.getGlobalInstancesIndex = do let a ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.instanceExtension a).discrTree

source

def Lean.Meta.getErasedInstances :

Lean.CoreM (Std.PHashSet Lean.Name)

Equations

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

source

structure Lean.Meta.DefaultInstanceEntry :

Type

className : Lean.Name
instanceName : Lean.Name
priority : Nat

source

@[inline]

abbrev Lean.Meta.PrioritySet :

Type

Equations

Lean.Meta.PrioritySet = Std.RBTree Nat fun x y => compare y x

source

structure Lean.Meta.DefaultInstances :

Type

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

source

instance Lean.Meta.instInhabitedDefaultInstances :

Inhabited Lean.Meta.DefaultInstances

Equations

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

source

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

Lean.Meta.DefaultInstances

Equations

Lean.Meta.addDefaultInstanceEntry d e = let d := { defaultInstances := d.defaultInstances, priorities := Std.RBTree.insert d.priorities e.priority }; match Lean.NameMap.find? d.defaultInstances e.className with | some insts => { defaultInstances := Lean.NameMap.insert d.defaultInstances e.className ((e.instanceName, e.priority) :: insts), priorities := d.priorities } | none => { defaultInstances := Lean.NameMap.insert d.defaultInstances e.className [(e.instanceName, e.priority)], priorities := d.priorities }

source

constant Lean.Meta.defaultInstanceExtension :

Lean.SimplePersistentEnvExtension Lean.Meta.DefaultInstanceEntry Lean.Meta.DefaultInstances

source

def Lean.Meta.addDefaultInstance (declName : Lean.Name) (prio : optParam Nat 0) :

Lean.MetaM Unit

Equations

Lean.Meta.addDefaultInstance declName prio = do let a ← Lean.getEnv match Lean.Environment.find? a declName with | none => Lean.throwError (Lean.toMessageData "unknown constant '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'") | some info => Lean.Meta.forallTelescopeReducing (Lean.ConstantInfo.type info) fun x type => match Lean.Expr.getAppFn type with | Lean.Expr.const className x x_1 => do let a ← Lean.getEnv let _do_jp : PUnit → Lean.MetaM Unit := fun y => do let a ← Lean.getEnv Lean.setEnv (Lean.PersistentEnvExtension.addEntry Lean.Meta.defaultInstanceExtension a { className := className, instanceName := declName, priority := prio }) if Lean.isClass a className = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid default instance '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', it has type '(" ++ Lean.toMessageData className ++ Lean.toMessageData " ...)', but " ++ Lean.toMessageData className ++ Lean.toMessageData "' is not a type class") _do_jp y | x => Lean.throwError (Lean.toMessageData "invalid default instance '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', type must be of the form '(C ...)' where 'C' is a type class")

source

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

m Lean.Meta.PrioritySet

Equations

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

source

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

m (List (Lean.Name × Nat))

Equations

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