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

Equations

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

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

Equations

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

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

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 : Lean.Format) (o : Lean.Options := { entries := [] }) : String

instance Lean.instToFormatName_lean : Lean.ToFormat Lean.Name

Equations

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

instance Lean.instToFormatDataValue : Lean.ToFormat Lean.DataValue

instance Lean.instToFormatProdNameDataValue : Lean.ToFormat (Lean.Name × Lean.DataValue)

def Lean.formatKVMap (m : Lean.KVMap) : Lean.Format

Equations

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

instance Lean.instToFormatKVMap : Lean.ToFormat Lean.KVMap

Equations

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