Equations
- instToFormat = { format := Std.Format.text ∘ toString }
Equations
- List.format x = match x with | [] => Std.Format.text "[]" | xs => Lean.Format.sbracket (Lean.Format.joinSep xs (Std.Format.text "," ++ Lean.Format.line))
Equations
- instToFormatList = { format := List.format }
Equations
- instToFormatArray = { format := fun a => Std.Format.text "#" ++ Lean.format (Array.toList a) }
Equations
- Option.format x = match x with | none => Std.Format.text "none" | some a => Std.Format.text "some " ++ Lean.format a
Equations
- instToFormatOption = { format := Option.format }
instance
instToFormatProd
{α : Type u}
{β : Type v}
[inst : Lean.ToFormat α]
[inst : Lean.ToFormat β]
:
Lean.ToFormat (α × β)
Equations
- instToFormatProd = { format := fun x => match x with | (a, b) => Lean.Format.paren (Lean.format a ++ Std.Format.text "," ++ Lean.Format.line ++ Lean.format b) }