Documentation

Lake.Toml.Data.Value

TOML Value #

inductive Lake.Toml.Value :

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

Instances For

instance Lake.Toml.instInhabitedValue :

Inhabited Value

Equations

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

instance Lake.Toml.instBEqValue :

Equations

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

@[reducible, inline]

abbrev Lake.Toml.Table :

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 :

Equations

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

@[inline]

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

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) :

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) :

Equations

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

def Lake.Toml.ppSimpleKey (k : 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) :

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

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

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

instance Lake.Toml.instToStringValue :

Equations

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

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

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) :

Equations

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