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 : Lake.Toml.RBDict Lean.Name Lake.Toml.Value Lean.Name.quickCmp) : Lake.Toml.Value

instance Lake.Toml.instInhabitedValue : Inhabited Value

Equations

• Lake.Toml.instInhabitedValue = { default := Lake.Toml.Value.string default default }

instance Lake.Toml.instBEqValue : BEq Value

Equations

• Lake.Toml.instBEqValue = { beq := Lake.Toml.beqValue✝ }

@[reducible, inline]

abbrev Lake.Toml.Table : Type

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

Equations

• Lake.Toml.Table = Lake.Toml.NameDict Lake.Toml.Value

@[inline]

def Lake.Toml.Table.empty : Table

Equations

• Lake.Toml.Table.empty = Lake.Toml.RBDict.empty

@[inline]

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

Equations

• Lake.Toml.Table.mkEmpty capacity = Lake.Toml.RBDict.mkEmpty capacity

@[reducible, match_pattern, inline]

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

Equations

• Lake.Toml.Value.table ref t = Lake.Toml.Value.table'✝ ref t

@[inline]

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

Equations

• (Lake.Toml.Value.string ref s).ref = ref
• (Lake.Toml.Value.integer ref n).ref = ref
• (Lake.Toml.Value.float ref n).ref = ref
• (Lake.Toml.Value.boolean ref b).ref = ref
• (Lake.Toml.Value.dateTime ref dt).ref = ref
• (Lake.Toml.Value.array ref xs).ref = ref
• (Lake.Toml.Value.table'✝ ref xs).ref = ref

Pretty Printing

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

Equations

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

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

Equations

• Lake.Toml.ppSimpleKey k = if (k.all fun (c : Char) => c.isAlphanum || c == '_' || c == '-') = true then k else Lake.Toml.ppString k

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

instance Lake.Toml.instToStringValue : ToString Value

Equations

• Lake.Toml.instToStringValue = { toString := Lake.Toml.Value.toString }

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

Equations

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

def Lake.Toml.ppTable.appendKeyval (s : String) (k : Lean.Name) (v : Value) : String

Equations

• Lake.Toml.ppTable.appendKeyval s k v = s.append (toString "" ++ toString (Lake.Toml.ppKey k) ++ toString " = " ++ toString v ++ toString "\n")