Documentation

Lean.Elab.Util

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

      Two names are from the same lexical scope if their scoping information modulo MacroScopesView.name is equal.

      Equations
      • a.equalScope b = (a.scopes == b.scopes && a.mainModule == b.mainModule && a.imported == b.imported)
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Instances For
            @[reducible, inline]
            Equations
            Instances For

              If ref does not have position information, then try to use macroStack

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]
                      unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrBuiltinName : Lake.Name) (attrName : Lake.Name) (parserNamespace : Lake.Name) (typeName : Lake.Name) (kind : String) (attrDeclName : autoParam Lake.Name _auto✝) :
                      Instances For
                        @[implemented_by Lean.Elab.mkMacroAttributeUnsafe]

                        Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful. Return none if all macros threw Macro.Exception.unsupportedSyntax.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Instances
                            @[always_inline]
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                partial def Lean.Elab.mkUnusedBaseName.loop (baseName : Lake.Name) (currNamespace : Lake.Name) (idx : Nat) :
                                Equations
                                Instances For

                                  If x throws an exception, catch it and turn it into a log message (using logException).

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