def Std.Format.getWidth (o : Lean.Options) : Nat

Equations

• Std.Format.getWidth o = o.get `format.width Std.Format.defWidth

def Std.Format.getIndent (o : Lean.Options) : Nat

Equations

• Std.Format.getIndent o = o.get `format.indent Std.Format.defIndent

def Std.Format.getUnicode (o : Lean.Options) : Bool

Equations

• Std.Format.getUnicode o = o.get `format.unicode Std.Format.defUnicode

opaque Std.Format.format.width : Lean.Option Nat

opaque Std.Format.format.unicode : Lean.Option Bool

opaque Std.Format.format.indent : Lean.Option Nat

def Std.Format.pretty' (f : Format) (o : Lean.Options := ∅) : String

Equations

• f.pretty' o = f.pretty (Lean.Option.get o Std.Format.format.width)

@[implicit_reducible]

instance Lean.instToFormatName_lean : ToFormat Name

Equations

• Lean.instToFormatName_lean = { format := fun (n : Lean.Name) => Std.Format.text n.toString }

@[implicit_reducible]

instance Lean.instToFormatDataValue : ToFormat DataValue

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.instToFormatProdNameDataValue : ToFormat (Name × DataValue)

Equations

• Lean.instToFormatProdNameDataValue = { format := fun (x : Lean.Name × Lean.DataValue) => match x with | (n, v) => Std.format n ++ Std.Format.text " := " ++ Std.format v }

def Lean.formatKVMap (m : KVMap) : Format

Equations

• Lean.formatKVMap m = (Std.Format.joinSep m.entries (Std.Format.text ", ")).sbracket

@[implicit_reducible]

instance Lean.instToFormatKVMap : ToFormat KVMap

Equations

• Lean.instToFormatKVMap = { format := Lean.formatKVMap }