@[implicit_reducible]

def Lean.instInhabitedThunk_batteries {α : Type u_1} [Inhabited α] : Inhabited (Thunk α)

Forward port of lean4#12469

Equations

• Lean.instInhabitedThunk_batteries = { default := Thunk.pure default }

def Lean.NameMapExtension (α : Type) : Type

Environment extension that maps declaration names to α. This uses a Thunk to avoid computing the name map when it isn't used.

Equations

• Lean.NameMapExtension α = Lean.SimplePersistentEnvExtension (Lean.Name × α) (Thunk (Lean.NameMap α))

@[implicit_reducible]

instance Lean.instInhabitedNameMapExtension {α : Type} : Inhabited (NameMapExtension α)

Equations

• Lean.instInhabitedNameMapExtension = { default := Lean.instInhabitedNameMapExtension._aux_1 }

def Lean.NameMapExtension.find? {α : Type} (ext : NameMapExtension α) (env : Environment) : Name → Option α

Look up a value in the given extension in the environment.

Equations

• ext.find? env = (Lean.SimplePersistentEnvExtension.getState ext env).get.find?

def Lean.NameMapExtension.add {M : Type → Type} {α : Type} [Monad M] [MonadEnv M] [MonadError M] (ext : NameMapExtension α) (k : Name) (v : α) : M Unit

Add the given k,v pair to the NameMapExtension.

Equations

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

def Lean.registerNameMapExtension (α : Type) (name : Name := by exact decl_name%) : IO (NameMapExtension α)

Registers a new extension with the given name and type.

Equations

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

structure Lean.NameMapAttributeImpl (α : Type) : Type

The inputs to registerNameMapAttribute.

• name : Name

  The name of the attribute

• ref : Name

  The declaration which creates the attribute

• descr : String

  The description of the attribute

• add (src : Name) (stx : Syntax) : AttrM α

  This function is called when the attribute is applied. It should produce a value of type α from the given attribute syntax.

def Lean.instInhabitedNameMapAttributeImpl.default {a✝ : Type} : NameMapAttributeImpl a✝

Equations

• Lean.instInhabitedNameMapAttributeImpl.default = { name := default, ref := default, descr := default, add := default }

@[implicit_reducible]

instance Lean.instInhabitedNameMapAttributeImpl {a✝ : Type} : Inhabited (NameMapAttributeImpl a✝)

Equations

• Lean.instInhabitedNameMapAttributeImpl = { default := Lean.instInhabitedNameMapAttributeImpl.default }

def Lean.registerNameMapAttribute {α : Type} (impl : NameMapAttributeImpl α) : IO (NameMapExtension α)

Similar to registerParametricAttribute except that attributes do not have to be assigned in the same file as the declaration.

Equations

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