@[instance 100]
Equations
- instToFormatOfToString = { format := Std.Format.text ∘ toString }
Equations
- x.format = match x with | [] => Std.Format.text "[]" | xs => (Lean.Format.joinSep xs (Std.Format.text "," ++ Lean.Format.line)).sbracket
Instances For
Equations
- instToFormatList = { format := List.format }
Equations
- instToFormatArray = { format := fun (a : Array α) => Std.Format.text "#" ++ Std.format a.toList }
Equations
- x.format = match x with | none => Std.Format.text "none" | some a => Std.Format.text "some " ++ Std.format a
Instances For
Equations
- instToFormatOption = { format := Option.format }
instance
instToFormatProd
{α : Type u}
{β : Type v}
[Lean.ToFormat α]
[Lean.ToFormat β]
:
Lean.ToFormat (α × β)
Equations
- instToFormatProd = { format := fun (x : α × β) => match x with | (a, b) => (Std.format a ++ Std.Format.text "," ++ Lean.Format.line ++ Std.format b).paren }
Equations
- s.toFormat = Lean.Format.joinSep (s.splitOn "\n") Lean.Format.line
Instances For
Equations
- instToFormatPos = { format := fun (p : String.Pos) => Std.format p.byteIdx }