Documentation

Init.Data.Format.Instances

instance instToFormat {α : Type u_1} [inst : ToString α] :

Std.ToFormat α

Equations

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

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

List α → Std.Format

Equations

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

instance instToFormatList {α : Type u_1} [inst : Std.ToFormat α] :

Std.ToFormat (List α)

Equations

instToFormatList = { format := List.format }

instance instToFormatArray {α : Type u_1} [inst : Std.ToFormat α] :

Std.ToFormat (Array α)

Equations

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

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

Option α → Std.Format

Equations

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

instance instToFormatOption {α : Type u} [inst : Std.ToFormat α] :

Std.ToFormat (Option α)

Equations

instToFormatOption = { format := Option.format }

instance instToFormatProd {α : Type u} {β : Type v} [inst : Std.ToFormat α] [inst : Std.ToFormat β] :

Std.ToFormat (α × β)

Equations

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

def String.toFormat (s : String) :

Equations

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

instance instToFormatPos :

Std.ToFormat String.Pos

Equations

instToFormatPos = { format := fun p => Std.format p.byteIdx }