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

Equations

• One or more equations did not get rendered due to their size.

Numerals

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

Equations

• Lake.Toml.decodeDecNum s = String.foldl (fun (n : Nat) (c : Char) => if (c == '_') = true then n else n * 10 + (c.val - '0'.val).toNat) 0 s

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

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

Equations

• Lake.Toml.decodeDecInt s = match Lake.Toml.decodeSign s with | (sign, s) => if sign = true then Int.negOfNat (Lake.Toml.decodeDecNum s) else Int.ofNat (Lake.Toml.decodeDecNum s)

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

Equations

• Lake.Toml.elabDecInt x = do let __do_lift ← Lake.Toml.elabLit x "decimal integer" pure (Lake.Toml.decodeDecInt __do_lift)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lake.Toml.elabFloat x = do let __do_lift ← Lake.Toml.elabLit x "float" pure (Lake.Toml.decodeFloat __do_lift)

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

Equations

• Lake.Toml.decodeHexDigit c = if c ≤ '9' then (c.val - '0'.val).toNat else if c ≤ 'F' then 10 + (c.val - 'A'.val).toNat else 10 + (c.val - 'a'.val).toNat

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 Lake.Toml.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

Equations

• Lake.Toml.dropInitialNewline s = if (s.front == '\x0d') = true then s.drop 2 else if (s.front == '\n') = true then s.drop 1 else s

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

Equations

• Lake.Toml.elabMlLiteralString x = do let spelling ← Lake.Toml.elabLit x "multi-line literal string" pure (Lake.Toml.dropInitialNewline ((spelling.drop 3).dropRight 3))

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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 Lake.Toml.Value) : Lean.CoreM Lake.Toml.Table

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