@[implicit_reducible, instance 100]

instance instToFormatOfToString {α : Type u_1} [ToString α] : Std.ToFormat α

def List.format {α : Type u_1} [Std.ToFormat α] : List α → Std.Format

@[implicit_reducible]

instance instToFormatList {α : Type u_1} [Std.ToFormat α] : Std.ToFormat (List α)

@[implicit_reducible]

instance instToFormatArray {α : Type u_1} [Std.ToFormat α] : Std.ToFormat (Array α)

def Option.format {α : Type u} [Std.ToFormat α] : Option α → Std.Format

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.

@[implicit_reducible]

instance instToFormatOption {α : Type u} [Std.ToFormat α] : Std.ToFormat (Option α)

@[implicit_reducible]

instance instToFormatProd {α : Type u} {β : Type v} [Std.ToFormat α] [Std.ToFormat β] : Std.ToFormat (α × β)

def String.toFormat (s : String) : Std.Format

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

@[implicit_reducible]

instance instToFormatRaw : Std.ToFormat String.Pos.Raw