Documentation

Lake.Toml.Elab.Value

TOML Value Elaboration #

Elaborates TOML values into Lean data types.

Numerals #

Strings & Simple Keys #

source
def Lake.Toml.elabSimpleKey (x : Lean.TSyntax `Lake.Toml.simpleKey) :
Lean.CoreM String
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Complex Values #

    source
    partial def Lake.Toml.elabVal (x : Lean.TSyntax `Lake.Toml.val) :
    Lean.CoreM Value