Documentation

Lean.AddDecl

Adds given declaration to the environment, respecting debug.skipKernelTC.

Equations
    Instances For
      @[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
      Equations
        Instances For

          Returns the kind of the declaration as originally declared instead of as exported. This information is stored by Lean.addDecl and may be inaccurate if that function was circumvented. Returns none if the declaration was not found.

          Equations
            Instances For

              Checks whether the declaration was originally declared as a theorem; see also Lean.getOriginalConstKind?. Returns false if the declaration was not found.

              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For