Documentation

Init.Data.Format.Instances

@[instance 100]
instance instToFormatOfToString {α : Type u_1} [ToString α] :
Equations
def List.format {α : Type u_1} [Lean.ToFormat α] :
Equations
Instances For
    instance instToFormatList {α : Type u_1} [Lean.ToFormat α] :
    Equations
    • instToFormatList = { format := List.format }
    instance instToFormatArray {α : Type u_1} [Lean.ToFormat α] :
    Equations
    Equations
    Instances For
      Equations
      • instToFormatOption = { format := Option.format }
      instance instToFormatProd {α : Type u} {β : Type v} [Lean.ToFormat α] [Lean.ToFormat β] :
      Equations
      Equations
      Instances For
        Equations