Documentation

Lean.Elab.Util

Equations
    Instances For
      Equations
        Instances For

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

          Equations
            Instances For
              Equations
                Instances For
                  Instances For
                    @[reducible, inline]
                    Equations
                      Instances For
                        def Lean.Elab.getBetterRef (ref : Syntax) (macroStack : MacroStack) :

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

                        Equations
                          Instances For
                            def Lean.Elab.addMacroStack {m : TypeType} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) :
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (stx : Syntax) :
                                        Equations
                                          Instances For
                                            @[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]
                                            unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrBuiltinName attrName parserNamespace typeName : Name) (kind : String) (attrDeclName : Name := by exact decl_name%) :
                                            Equations
                                              Instances For
                                                Equations
                                                  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
                                                      Instances For
                                                        Instances
                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      partial def Lean.Elab.mkUnusedBaseName.loop (baseName currNamespace : 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
                                                                                Instances For
                                                                                  def Lean.Elab.throwErrorWithNestedErrors {m : TypeType} {α : Type} [MonadError m] [Monad m] [MonadLog m] (msg : MessageData) (exs : Array Exception) :
                                                                                  m α
                                                                                  Equations
                                                                                    Instances For