TOML Value Elaboration

Elaborates TOML values into Lean data types.

@[inline]

def Lake.Toml.elabLit {k : Lean.SyntaxNodeKind} (x : Lean.TSyntax k) (name : String) : Lean.CoreM String

def Lake.Toml.elabBoolean (x : Lean.TSyntax `Lake.Toml.boolean) : Lean.CoreM Bool

Numerals

def Lake.Toml.decodeDecNum (s : String) : Nat

def Lake.Toml.decodeSign (s : String) : Bool × String

def Lake.Toml.decodeDecInt (s : String) : Int

def Lake.Toml.elabDecInt (x : Lean.TSyntax `Lake.Toml.decInt) : Lean.CoreM Int

def Lake.Toml.decodeMantissa (s : String) : Nat × Nat

def Lake.Toml.decodeFrExp (s : String) : Nat × Int

def Lake.Toml.decodeFloat (s : String) : Float

def Lake.Toml.elabFloat (x : Lean.TSyntax `Lake.Toml.float) : Lean.CoreM Float

def Lake.Toml.elabBinNum (x : Lean.TSyntax `Lake.Toml.binNum) : Lean.CoreM Nat

def Lake.Toml.elabOctNum (x : Lean.TSyntax `Lake.Toml.octNum) : Lean.CoreM Nat

def Lake.Toml.decodeHexDigit (c : Char) : Nat

def Lake.Toml.elabHexNum (x : Lean.TSyntax `Lake.Toml.hexNum) : Lean.CoreM Nat

def Lake.Toml.elabDateTime (x : Lean.TSyntax `Lake.Toml.dateTime) : Lean.CoreM DateTime

Strings & Simple Keys

def Lake.Toml.elabLiteralString (x : Lean.TSyntax `Lake.Toml.literalString) : Lean.CoreM String

def Lake.Toml.decodeHexDigits (s : Substring) : Nat

partial def Lake.Toml.elabBasicStringCore (lit : String) (i : String.Pos := 0) (out : String := "") : Lean.CoreM String

def Lake.Toml.elabBasicString (x : Lean.TSyntax `Lake.Toml.basicString) : Lean.CoreM String

def Lake.Toml.dropInitialNewline (s : String) : String

def Lake.Toml.elabMlLiteralString (x : Lean.TSyntax `Lake.Toml.mlLiteralString) : Lean.CoreM String

def Lake.Toml.elabMlBasicString (x : Lean.TSyntax `Lake.Toml.mlBasicString) : Lean.CoreM String

def Lake.Toml.elabString (x : Lean.TSyntax `Lake.Toml.string) : Lean.CoreM String

@[inline]

def Lake.Toml.elabUnquotedKey (x : Lean.TSyntax `Lake.Toml.unquotedKey) : Lean.CoreM String

def Lake.Toml.elabSimpleKey (x : Lean.TSyntax `Lake.Toml.simpleKey) : Lean.CoreM String

Complex Values

def Lake.Toml.elabArray {α : Type} (x : Lean.TSyntax `Lake.Toml.array) (elabVal : Lean.TSyntax `Lake.Toml.val → Lean.CoreM α) : Lean.CoreM (Array α)

def Lake.Toml.elabInlineTable (x : Lean.TSyntax `Lake.Toml.inlineTable) (elabVal : Lean.TSyntax `Lake.Toml.val → Lean.CoreM Value) : Lean.CoreM Table

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