@[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

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

Equations

• instToFormatList = { format := List.format }

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

Equations

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

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

Equations

• instToFormatOption = { format := Option.format }

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

Equations

• s.toFormat = Std.Format.joinSep (s.splitOn "\n") Std.Format.line

instance instToFormatPos : Std.ToFormat String.Pos

Equations

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