Documentation

Init.Data.Format.Basic

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

Instances For
    inductive Std.Format :

    A string with pretty-printing information for rendering in a column-width-aware way.

    The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

    Instances For

      Check whether the given format contains no characters.

      Equations
      Instances For

        Alias for a group with FlattenBehavior set to fill.

        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations

              A monad in which we can pretty-print Format objects.

              • pushOutput : Stringm Unit
              • pushNewline : Natm Unit
              • currColumn : m Nat
              • startTag : Natm Unit

                Start a scope tagged with n.

              • endTags : Natm Unit

                Exit the scope of n-many opened tags.

              Instances
                def Std.Format.prettyM {m : TypeType} (f : Lean.Format) (w : Nat) (indent : optParam Nat 0) [Monad m] [Std.Format.MonadPrettyFormat m] :

                Render the given f : Format with a line width of w. indent is the starting amount to indent each line by.

                Equations
                Instances For
                  @[inline]

                  Create a format l ++ f ++ r with a flatten group. FlattenBehaviour is allOrNone; for fill use bracketFill.

                  Equations
                  Instances For
                    @[inline]

                    Creates the format "(" ++ f ++ ")" with a flattening group.

                    Equations
                    Instances For
                      @[inline]

                      Creates the format "[" ++ f ++ "]" with a flattening group.

                      Equations
                      Instances For
                        @[inline]

                        Same as bracket except uses the fill flattening behaviour.

                        Equations
                        Instances For

                          Default indentation.

                          Equations
                          Instances For

                            Default width of the targeted output pane.

                            Equations
                            Instances For

                              Nest with the default indentation amount.

                              Equations
                              Instances For

                                Insert a newline and then f, all nested by the default indent amount.

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

                                  Renders a Format to a string.

                                  • width: the total width
                                  • indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)
                                  • column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)
                                  Equations
                                  • f.pretty width indent column = (f.prettyM width indent { out := "", column := column }).snd.out
                                  Instances For
                                    class Std.ToFormat (α : Type u) :

                                    Class for converting a given type α to a Format object for pretty-printing. See also Repr, which also outputs a Format object.

                                    Instances

                                      Intersperse the given list (each item printed with format) with the given sep format.

                                      Equations
                                      Instances For

                                        Format each item in items and prepend prefix pre.

                                        Equations
                                        Instances For

                                          Format each item in items and append suffix.

                                          Equations
                                          Instances For