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

Equations

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

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

Equations

• Lake.Toml.decodeSign s = if (s.front == '-') = true then (true, s.drop 1) else if (s.front == '+') = true then (false, s.drop 1) else (false, s)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Strings & Simple Keys

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

Equations

• Lake.Toml.elabLiteralString x = do let __do_lift ← Lake.Toml.elabLit x "literalString" pure ((__do_lift.drop 1).dropRight 1)

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

Equations

• Lake.Toml.decodeHexDigits s = Substring.foldl (fun (n : Nat) (c : Char) => n * 16 + Lake.Toml.decodeHexDigit c) 0 s

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

Equations

• Lake.Toml.elabBasicString x = do let spelling ← Lake.Toml.elabLit x "basic string" Lean.withRef x.raw (Lake.Toml.elabBasicStringCore ((spelling.drop 1).dropRight 1))

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

Equations

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

@[inline]

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

Equations

• Lake.Toml.elabUnquotedKey x = Lake.Toml.elabLit x "unquoted key"

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 α)

Equations

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

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

Equations

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

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