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
Equations
- Lake.Toml.instInhabitedValue = { default := Lake.Toml.Value.string default default }
Equations
- Lake.Toml.instBEqValue = { beq := Lake.Toml.beqValue✝ }
@[reducible, inline]
A TOML table, an ordered key-value map of TOML values (Lake.Toml.Value
).
Instances For
@[inline]
Equations
Instances For
@[inline]
Instances For
@[reducible, match_pattern, inline]
Instances For
@[inline]
Equations
Instances For
Pretty Printing #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Toml.instToStringValue = { toString := Lake.Toml.Value.toString }
Equations
- One or more equations did not get rendered due to their size.