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
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For

              Similar to resolveGlobalName, but also executes reserved name actions.

              Equations
                Instances For

                  Similar to resolveGlobalConstCore, but also executes reserved name actions.

                  Equations
                    Instances For

                      Similar to realizeGlobalConstNoOverloadCore, but also executes reserved name actions.

                      Equations
                        Instances For

                          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
                            Instances For

                              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
                                Instances For