Documentation

Lean.Message

def Lean.mkErrorStringWithPos (fileName : String) (pos : Lean.Position) (msg : String) (endPos : optParam (Option Lean.Position) none) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A naming context is the information needed to shorten names in pretty printing.

    It gives the current namespace and the list of open declarations.

    Instances For
      structure Lean.PPFormat :

      Lazily formatted text to be used in MessageData.

      Instances For

        Structured message data. We use it for reporting errors, trace messages, etc.

        Instances For

          Returns true when the message contains a MessageData.tagged tag .. constructor where p tag is true.

          Equations
          • Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
          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
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.

                    Wrap the given message in l and r. See also Format.bracket.

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

                      Wrap the given message in parentheses ().

                      Equations
                      Instances For

                        Wrap the given message in square brackets [].

                        Equations
                        Instances For

                          Write the given list of messages as a list, separating each item with ,\n and surrounding with square brackets.

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

                            A Message is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows.

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

                                A persistent array of messages.

                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        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
                                              def Lean.MessageLog.forM {m : TypeType} [Monad m] (log : Lean.MessageLog) (f : Lean.Messagem Unit) :
                                              Equations
                                              Instances For
                                                Equations
                                                Instances For
                                                  Instances
                                                    Equations
                                                    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
                                                        Instances
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            Equations
                                                            Equations
                                                            Equations
                                                            Equations
                                                            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.
                                                            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