@[implicit_reducible, instance 100]

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

Equations

• instToFormatOfToString = { format := Std.Format.text ∘ toString }

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

Equations

• [].format = Std.Format.text "[]"
• x✝.format = (Std.Format.joinSep x✝ (Std.Format.text "," ++ Std.Format.line)).sbracket

@[implicit_reducible]

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

Equations

• instToFormatList = { format := List.format }

@[implicit_reducible]

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

Equations

• instToFormatArray = { format := fun (a : Array α) => Std.Format.text "#" ++ Std.format a.toList }

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.

Equations

• none.format = Std.Format.text "none"
• (some a).format = Std.Format.text "some " ++ Std.format a

@[implicit_reducible]

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

Equations

• instToFormatOption = { format := Option.format }

@[implicit_reducible]

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

Equations

• instToFormatProd = { format := fun (x : α × β) => match x with | (a, b) => (Std.format a ++ Std.Format.text "," ++ Std.Format.line ++ Std.format b).paren }

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

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

Equations

• s.toFormat = Std.Format.joinSep (s.split '\n').toList Std.Format.line

@[implicit_reducible]

instance instToFormatRaw : Std.ToFormat String.Pos.Raw

Equations

• instToFormatRaw = { format := fun (p : String.Pos.Raw) => Std.format p.byteIdx }