def Lean.ReservedNameAction : Type

When trying to resolve a reserved name, an action can be executed to generate the actual definition/theorem. The action returns true if it "handled" the given name.

Remark: usually when one install a reserved name predicate, an associated action is also installed.

def Lean.registerReservedNameAction (act : ReservedNameAction) : IO Unit

Register a new function that is invoked when trying to resolve a reserved name.

def Lean.executeReservedNameAction (name : Name) : CoreM Unit

Execute a registered reserved action for the given reserved name. Note that the handler can throw an exception.

def Lean.realizeGlobalName (id : Name) : CoreM (List (Name × List String))

Similar to resolveGlobalName, but also executes reserved name actions.

def Lean.realizeGlobalConstCore (n : Name) : CoreM (List Name)

Similar to resolveGlobalConstCore, but also executes reserved name actions.

def Lean.realizeGlobalConstNoOverloadCore (n : Name) : CoreM Name

Similar to realizeGlobalConstNoOverloadCore, but also executes reserved name actions.

def Lean.realizeGlobalConst (stx : Syntax) : CoreM (List Name)

Similar to resolveGlobalConst, but also executes reserved name actions.

Consider using realizeGlobalConstWithInfo if you want the syntax to show the resulting name's info on hover.

def Lean.realizeGlobalConstNoOverload (id : Syntax) : CoreM Name

Similar to realizeGlobalConstNoOverload, but also executes reserved name actions.

Consider using realizeGlobalConstNoOverloadWithInfo if you want the syntax to show the resulting name's info on hover.