Documentation

Lake.Toml.Elab.Expression

TOML Expression Elaboration #

Elaborates top-level TOML syntax into a Lean Toml.Table.

The manner in which a TOML key was declared.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Instances For
        Equations
        • Lake.Toml.instInhabitedElabState = { default := { keyTys := default, arrKeyTys := default, arrParents := default, currArrKey := default, currKey := default, items := default } }
        @[reducible, inline]
        Equations
        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
                        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