Documentation

Lean.PrettyPrinter

def Lean.PPContext.runCoreM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.CoreM α) :
IO α
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Lean.PPContext.runMetaM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.MetaM α) :
    IO α
    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
        • One or more equations did not get rendered due to their size.
        Instances For

          Return a fmt representing pretty-printed e together with a map from tags in fmt to Elab.Info nodes produced by the delaborator at various subexpressions of e.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[export lean_pp_expr]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Pretty-prints a declaration c as c.{<levels>} <params> : <type>.

              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

                  Turns a MetaM FormatWithInfos into a MessageData.lazy which will run the monadic value. Uses the pp.tagAppFns option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover.

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

                    Turns a MetaM MessageData into a MessageData.lazy which will run the monadic value. The optional array of expressions is used to set the hasSyntheticSorry fields, and should comprise the expressions that are included in the message data.

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

                      Pretty print a const expression using delabConst and generate terminfo. This function avoids inserting @ if the constant is for a function whose first argument is implicit, which is what the default toMessageData for Expr does. Panics if e is not a constant.

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

                        Generates MessageData for a declaration c as c.{<levels>} <params> : <type>, with terminfo.

                        Equations
                        Instances For