instance instToFormat {α : Type u_1} [ToString α] : Lean.ToFormat α

Equations

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

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

Equations

• List.format x = match x with | [] => Std.Format.text "[]" | xs => Lean.Format.sbracket (Lean.Format.joinSep xs (Std.Format.text "," ++ Lean.Format.line))

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

Equations

• instToFormatList = { format := List.format }

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

Equations

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

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

Equations

• Option.format x = match x with | none => Std.Format.text "none" | some a => Std.Format.text "some " ++ Std.format a

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

Equations

• instToFormatOption = { format := Option.format }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

instance instToFormatPos : Lean.ToFormat String.Pos

Equations

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