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
@[reducible, inline]
A TOML table, an ordered key-value map of TOML values (Lake.Toml.Value
).
Equations
Instances For
@[reducible, match_pattern, inline]