Documentation

Init.Data.Format.Instances

instance instToFormat {α : Type u_1} [inst : ToString α] :
Equations
def List.format {α : Type u_1} [inst : Lean.ToFormat α] :
Equations
instance instToFormatList {α : Type u_1} [inst : Lean.ToFormat α] :
Equations
  • instToFormatList = { format := List.format }
instance instToFormatArray {α : Type u_1} [inst : Lean.ToFormat α] :
Equations
def Option.format {α : Type u} [inst : Lean.ToFormat α] :
Equations
instance instToFormatOption {α : Type u} [inst : Lean.ToFormat α] :
Equations
  • instToFormatOption = { format := Option.format }
instance instToFormatProd {α : Type u} {β : Type v} [inst : Lean.ToFormat α] [inst : Lean.ToFormat β] :
Equations