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

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

Instances For

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

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

Instances For

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

- Std.Format.getUnicode o = Lean.KVMap.get o `format.unicode Std.Format.defUnicode

Instances For

source
opaque Std.Format.format.width :
Lean.Option Nat
source
opaque Std.Format.format.unicode :
Lean.Option Bool
source
opaque Std.Format.format.indent :
Lean.Option Nat
source
def Std.Format.pretty' (f : Format) (o : Lean.Options := { }) :
String
Equations

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

Instances For

source
instance Lean.instToFormatName_lean :
ToFormat Name
Equations

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

source
instance Lean.instToFormatDataValue :
ToFormat DataValue
Equations

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

source
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 }

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

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

Instances For

source
instance Lean.instToFormatKVMap :
ToFormat KVMap
Equations

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