TOML Value

inductive Lake.Toml.Value : Type

A TOML value with optional source info.

• string (ref : Lean.Syntax) (s : String) : Value
• integer (ref : Lean.Syntax) (n : Int) : Value
• float (ref : Lean.Syntax) (n : Float) : Value
• boolean (ref : Lean.Syntax) (b : Bool) : Value
• dateTime (ref : Lean.Syntax) (dt : DateTime) : Value
• array (ref : Lean.Syntax) (xs : Array Value) : Value
• table' (ref : Lean.Syntax) (xs : RBDict Lean.Name Value Lean.Name.quickCmp) : Value

def Lake.Toml.instInhabitedValue.default : Value

@[implicit_reducible]

instance Lake.Toml.instInhabitedValue : Inhabited Value

partial def Lake.Toml.instBEqValue.beq : Value → Value → Bool

@[implicit_reducible]

instance Lake.Toml.instBEqValue : BEq Value

@[reducible, inline]

abbrev Lake.Toml.Table : Type

A TOML table, an ordered key-value map of TOML values (Lake.Toml.Value).

@[inline]

def Lake.Toml.Table.empty : Table

@[inline]

def Lake.Toml.Table.mkEmpty (capacity : Nat) : Table

@[reducible, match_pattern, inline]

abbrev Lake.Toml.Value.table (ref : Lean.Syntax) (t : Table) : Value

@[inline]

def Lake.Toml.Value.ref : Value → Lean.Syntax

Pretty Printing

def Lake.Toml.ppString (s : String) : String

def Lake.Toml.ppSimpleKey (k : String) : String

partial def Lake.Toml.ppKey (k : Lean.Name) : String

partial def Lake.Toml.ppInlineTable (t : Table) : String

partial def Lake.Toml.ppInlineArray (vs : Array Value) : String

partial def Lake.Toml.Value.toString (v : Value) : String

@[implicit_reducible]

instance Lake.Toml.instToStringValue : ToString Value

def Lake.Toml.ppTable (t : Table) : String