Documentation

Lake.Toml.Data.Value

TOML Value #

inductive Lake.Toml.Value :

A TOML value with optional source info.

string: Lean.Syntax → String → Lake.Toml.Value
integer: Lean.Syntax → Int → Lake.Toml.Value
float: Lean.Syntax → Float → Lake.Toml.Value
boolean: Lean.Syntax → Bool → Lake.Toml.Value
dateTime: Lean.Syntax → Lake.Toml.DateTime → Lake.Toml.Value
array: Lean.Syntax → Array Lake.Toml.Value → Lake.Toml.Value
table': Lean.Syntax → Lake.Toml.RBDict Lake.Name Lake.Toml.Value Lean.Name.quickCmp → Lake.Toml.Value

Instances For

instance Lake.Toml.instInhabitedValue :

Inhabited Lake.Toml.Value

Equations

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

instance Lake.Toml.instBEqValue :

BEq Lake.Toml.Value

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 :

Lake.Toml.Table

Equations

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

@[inline]

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

Lake.Toml.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 : Lake.Toml.Table) :

Lake.Toml.Value

Equations

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

@[inline]

def Lake.Toml.Value.ref :

Lake.Toml.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 : Lake.Name) :

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

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

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

instance Lake.Toml.instToStringValue :

ToString Lake.Toml.Value

Equations

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

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

Equations

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

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

Equations

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