Documentation

Lake.Toml.Grammar

TOML Grammar #

A Lean encoding of the v1.0.0 TOML grammar (en, [abnf]]2) using Lean.Parser objects. The current encoding elides the use of tokens entirely, relying purely on custom parser functions.

Is it a TOML control character? (excludes tabs and spaces)

Equations

Trailing Functions #

Consume optional horizontal whitespace (i.e., tab or space).

Equations

Consumes the LF following a CR in a CRLF newline.

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

Consumes the body of a comment.

Consumes a line comment.

Consume optional whitespace (space, tab, or newline).

Consume optional sequence of whitespace / newline(s) / comment (s).

Strings #

A TOML character escape.

Consumes a TOML string escape sequence after a \.

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

Numerals (Date-Times, Floats, and Integers) #

@[inline]
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
partial def Lake.Toml.decNumberSepFn (startPos : String.Pos) (curr : Char) (nextPos : String.Pos) :
Equations
Equations
  • One or more equations did not get rendered due to their size.

Parsers #

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