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.

Equations

• Lean.ReservedNameAction = (Lake.Name → Lean.CoreM Bool)

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

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

Equations

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

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

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

Equations

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

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

Similar to resolveGlobalName, but also executes reserved name actions.

Equations

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

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

Similar to resolveGlobalConstCore, but also executes reserved name actions.

Equations

• Lean.realizeGlobalConstCore n = do let cs ← Lean.realizeGlobalName n Lean.filterFieldList n cs

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

Similar to realizeGlobalConstNoOverloadCore, but also executes reserved name actions.

Equations

• Lean.realizeGlobalConstNoOverloadCore n = do let __do_lift ← Lean.realizeGlobalConstCore n Lean.ensureNoOverload n __do_lift

def Lean.realizeGlobalConst (stx : Lean.Syntax) : Lean.CoreM (List Lake.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.

Equations

• Lean.realizeGlobalConst stx = Lean.withRef stx (Lean.preprocessSyntaxAndResolve stx Lean.realizeGlobalConstCore)

def Lean.realizeGlobalConstNoOverload (id : Lean.Syntax) : Lean.CoreM Lake.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.

Equations

• Lean.realizeGlobalConstNoOverload id = do let __do_lift ← Lean.realizeGlobalConst id Lean.ensureNonAmbiguous id __do_lift