Pieces the LaTeX and Typst spellings share
The two surfaces (Esm.Document.Math.Latex
, Esm.Document.Math.Typst
) differ in their
keyword spellings and lexers, but read numbers alike: a number in its JSON spelling, or a
scientific literal mantissa × 10^exponent, where only the spelling of × 10^ and of
the exponent’s brackets differs. lexNum
takes that difference as a parameter
(sciExp, which reads the tail after the mantissa), so the literal rule is written and
proved once:
- the tail is read with any amount of white space (none included) between its parts, so spacing never changes what is read;
- a mantissa (with or without a decimal point) followed by a complete tail is one
literal; a tail whose exponent is not an integer (
10^{n}) leaves the number alone, and the rest reads as an ordinary product.
A leading - belongs to the number only when its value is below zero (lexSigned
):
-0 reads as a minus sign and 0. Whether a negative literal is a literal or a binary
minus depends on what precedes it, which the parser decides (Esm.Document.Math.Parse
,
addLoop).
Literal prefixes
Spacing
Numbers
def sciSplit : JNum → Option (List Char × Int)
The mantissa (with its sign) and exponent of a number printed in scientific notation.
def sciNum (n0 : JNum) (z : Int) : Option JNum
The value of a mantissa (as Number.parseRaw
reads it, an integer or a decimal)
times 10^z, in canonical form; none for a value with no canonical form.
def lexNum (sciExp : List Char → Option (Int × List Char)) (cs : List Char) :
Option (Tok × List Char)
A number: its JSON spelling, or a decimal mantissa followed by a scientific tail that
sciExp reads (returning the exponent and what follows). The token ends where the number
as written ends (Number.parseRaw
); its value is the canonical form.
def lexSigned (sciExp : List Char → Option (Int × List Char)) (cs : List Char) :
Option (Tok × List Char)
A number at the front of the input, where - starts it only when the value is below
zero (otherwise the - is a minus sign of its own).
Reading numbers back
theorem lexNum_plain (sciExp : List Char → Option (Int × List Char)) (n : JNum) (hn : n.WF)
(X : List Char) (hX : Number.NumStop X) (hs : sciExp X = none) :
lexNum sciExp (Number.print n ++ X) = some (.num n, X)
A number in its JSON spelling, before a tail that is not scientific.
theorem lexNum_sci (sciExp : List Char → Option (Int × List Char)) (n : JNum) (hn : n.WF)
(m : List Char) (e : Int) (hsp : sciSplit n = some (m, e)) (T X : List Char)
(hT : sciExp T = some (e, X)) (hTh : ∀ c ∈ T.head?, c.isDigit = false ∧ c ≠ 'e') :
lexNum sciExp (m ++ T) = some (.num n, X)
A number in scientific spelling: its mantissa, then a tail sciExp reads as its
exponent.
theorem lexSigned_of (sciExp : List Char → Option (Int × List Char)) (N X : List Char) (n : JNum)
(hN : N ≠ []) (hneg : ∀ r, N = '-' :: r → negNum n = true)
(h : lexNum sciExp (N ++ X) = some (.num n, X)) : lexSigned sciExp (N ++ X) = some (.num n, X)
A number spelled N reads back with its sign: a spelling that starts with - is
of a negative number.