Documentation

Init.Data.Format.Instances

@[instance 100]
instance instToFormatOfToString {α : Type u_1} [ToString α] :
Equations
    def List.format {α : Type u_1} [Std.ToFormat α] :
    Equations
      Instances For
        instance instToFormatList {α : Type u_1} [Std.ToFormat α] :
        Equations
          instance instToFormatArray {α : Type u_1} [Std.ToFormat α] :
          Equations
            def Option.format {α : Type u} [Std.ToFormat α] :

            Formats an optional value, with no expectation that the Lean parser should be able to parse the result.

            This function is usually accessed through the ToFormat (Option α) instance.

            Equations
              Instances For
                Equations
                  instance instToFormatProd {α : Type u} {β : Type v} [Std.ToFormat α] [Std.ToFormat β] :
                  Equations

                    Converts a string to a pretty-printer document, replacing newlines in the string with Std.Format.line.

                    Equations
                      Instances For