Documentation

Lean.ReservedNameAction

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

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.

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.

Similar to resolveGlobalName, but also executes reserved name actions.

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

Similar to resolveGlobalConstCore, but also executes reserved name actions.

Equations

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

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