Documentation

Lean.Data.Format

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

Equations

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

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

Equations

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

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

Equations

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

constant Std.Format.format.width :

Lean.Option Nat

constant Std.Format.format.unicode :

Lean.Option Bool

constant Std.Format.format.indent :

Lean.Option Nat

def Std.Format.pretty' (f : Lean.Format) (o : optParam Lean.Options { entries := [] }) :

Equations

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

instance Lean.instToFormatName :

Lean.ToFormat Lean.Name

Equations

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

instance Lean.instToFormatDataValue :

Lean.ToFormat Lean.DataValue

Equations

Lean.instToFormatDataValue = { format := fun x => match x with | Lean.DataValue.ofString v => Lean.format (repr v) | Lean.DataValue.ofBool v => Lean.format v | Lean.DataValue.ofName v => Std.Format.text "`" ++ Lean.format v | Lean.DataValue.ofNat v => Lean.format v | Lean.DataValue.ofInt v => Lean.format v | Lean.DataValue.ofSyntax v => Lean.format v }

instance Lean.instToFormatProdNameDataValue :

Lean.ToFormat (Lean.Name × Lean.DataValue)

Equations

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

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

Equations

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

instance Lean.instToFormatKVMap :

Lean.ToFormat Lean.KVMap

Equations

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