TOML Expression Elaboration #
Elaborates top-level TOML syntax into a Lean Toml.Table
.
The manner in which a TOML key was declared.
- value: Lake.Toml.KeyTy
A key declared via
key = v
. - stdTable: Lake.Toml.KeyTy
A key declared via
[key]
. - array: Lake.Toml.KeyTy
A key declared via
[[key]]
. - dottedPrefix: Lake.Toml.KeyTy
A key declared via
key.foo
. - headerPrefix: Lake.Toml.KeyTy
A key declared via
[key.foo]
or[[key.foo]]
.
Instances For
Equations
- Lake.Toml.instInhabitedKeyTy = { default := Lake.Toml.KeyTy.value }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Toml.instToStringKeyTy = { toString := Lake.Toml.KeyTy.toString }
Equations
- ty.isValidPrefix = match ty with | Lake.Toml.KeyTy.stdTable => true | Lake.Toml.KeyTy.headerPrefix => true | Lake.Toml.KeyTy.dottedPrefix => true | x => false
Instances For
- ref : Lean.Syntax
- key : Lake.Name
- val : Lake.Toml.Value
Instances For
- keyTys : Lake.NameMap Lake.Toml.KeyTy
- arrKeyTys : Lake.NameMap (Lake.NameMap Lake.Toml.KeyTy)
- arrParents : Lake.NameMap Lake.Name
- currArrKey : Lake.Name
- currKey : Lake.Name
- items : Array Lake.Toml.Keyval
Instances For
Equations
- Lake.Toml.instInhabitedElabState = { default := { keyTys := default, arrKeyTys := default, arrParents := default, currArrKey := default, currKey := default, items := default } }
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct a table of simple key-value pairs from arbitrary key-value pairs.
For example:
{a.b := [c.d := 0]}, {a.b := [c.e := 1]}
becomes
{a := {b := [{c := {d := 0, e := 1}}]}}
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Lake.Toml.mkSimpleTable.insert
(t : Lake.Toml.Table)
(kRef : Lean.Syntax)
(k : Lake.Name)
(ks : List Lake.Name)
(newV : Lake.Toml.Value)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.