Accepted variants and refused spellings

theorem variant_bigl (X : List Char) :
    Latex.lexOne ('\\' :: ("bigl".toList ++ '(' :: X)) = Latex.lexOne ('\\' :: ("left".toList ++ '(' :: X))

\bigl( and \Bigl( read as the grouping \left(.

theorem variant_bigr (X : List Char) :
    Latex.lexOne ('\\' :: ("bigr".toList ++ ')' :: X)) = Latex.lexOne ('\\' :: ("right".toList ++ ')' :: X))

\bigr) reads as the grouping \right).

theorem variant_thickspace (n : Nat) (X : List Char) :
    Latex.skipWs (n + 1) ('\\' :: ';' :: X) = Latex.skipWs n X

The spacing command \; is skipped like a space.

theorem variant_times (c : Ctx) (f : Nat) (acc : List Json) (r : List Tok) :
    mulLoop c (f + 1) acc (.kw .times :: r) = mulLoop c (f + 1) acc (.kw .cdot :: r)

\times reads as the product \cdot.

theorem variant_dot (c : Ctx) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 1) (.kw .dotacc :: .kw .lb :: ((pr c a).at c.sf 1 ++ .kw .rb :: rest)) =
      some (dNode a "t", rest)

\dot{x} (LaTeX) reads as the time derivative of x.

theorem variant_dot_typst (c : Ctx) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 1) (.kw .cdot :: .kw .lp :: ((pr c a).at c.sf 1 ++ .kw .rp :: rest)) =
      some (dNode a "t", rest)

Typst dot(x) reads as the time derivative of x.

theorem variant_brackets (c : Ctx) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 1) (.kw .lbk :: ((pr c a).at c.sf 1 ++ .kw .rbk :: rest)) = some (a, rest)

[x] reads as the grouping (x).

theorem variant_log (c : Ctx) (f : Nat) (r : List Tok) :
    pPrim c (f + 1) (.kw .log :: .kw .lp :: r) = pPrim c (f + 1) (.kw .ln :: .kw .lp :: r)

\log(x) reads as \ln(x).

theorem variant_euler (c : Ctx) (hc : c.sf = .latex) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 3) (.rm "e" :: .kw .caret :: .kw .lb :: ((pr c a).at c.sf 1 ++ .kw .rb :: rest)) =
      some (node "exp" [a], rest)

\mathrm{e}^{x} (LaTeX) reads as \exp(x).

theorem variant_pow (c : Ctx) (x y : Json) (hx : M c x) (hy : M c y) (rest : List Tok) (f : Nat)
    (hf : need 1 (sepBy [.kw .comma] ([x, y].map fun z => (pr c z).at c.sf 4)).length + 3 ≤ f) :
    pOpn c (f + 1) "pow" (.kw .lp :: (sepBy [.kw .comma] ([x, y].map fun z => (pr c z).at c.sf 4) ++
      .kw .rp :: rest)) = some (node "^" [x, y], rest)

The deprecated call form \operatorname{pow}(x, y) reads as the power x^{y}.

theorem variant_neg (c : Ctx) (x : Json) (hx : M c x) (rest : List Tok) (f : Nat)
    (hf : need 1 (sepBy [.kw .comma] ([x].map fun z => (pr c z).at c.sf 4)).length + 3 ≤ f) :
    pOpn c (f + 1) "neg" (.kw .lp :: (sepBy [.kw .comma] ([x].map fun z => (pr c z).at c.sf 4) ++
      .kw .rp :: rest)) = some (node "-" [x], rest)

The deprecated call form \operatorname{neg}(x) reads as the negation -x.

theorem variant_thinspace (n : Nat) (X : List Char) (hX : Latex.unitTok X = none) :
    Latex.skipWs (n + 1) ('\\' :: ',' :: X) = Latex.skipWs n X

The spacing command \, is skipped like a space where no unit follows it (k\,T); before \mathrm{…} spelling a unit it is the quantity’s unit separator.

theorem variant_sci_spacing (c : Char) (r : List Char) (h : Latex.isWsL c = true) :
    Latex.sciExp (c :: r) = Latex.sciExp r

A scientific literal reads the same with any spacing around \times, 10, ^ and the braces, none included: the tail after the mantissa is read past white space and the spacing commands (Latex.skipSp ), so 2\times10^{3} and 2 \times 10^{3} are the literal 2 \times 10^{3} is.

theorem variant_sci_spacing_typst (c : Char) (r : List Char) (h : Typst.isWsT c = true) :
    Typst.sciExp (c :: r) = Typst.sciExp r

Typst: the same for times 10^(…).

theorem variant_minus_literal (c : Ctx) (f : Nat) (acc : List Json) (n : JNum) (r : List Tok)
    (hn : negNum n = true) (hw : (negate n).wfb = true) :
    addLoop c (f + 1) acc (.num n :: r) = addLoop c (f + 1) acc (.kw .minus :: .num (negate n) :: r)

A negative literal right after an operand (k-1, k -1) reads as a binary minus and the positive number, the same as k - 1.

theorem variant_paren (c : Ctx) (f : Nat) (r : List Tok) :
    pPrim c (f + 1) (.kw .lp :: r) = pPrim c (f + 1) (.kw .lpg :: r)

A plain ( in LaTeX groups like \left( (a primary’s ( reads alike on both surfaces).

theorem variant_italic_d (c : Ctx) (hc : c.sf = .latex) (n : String) (hd : c.S.names.contains "d" = false)
    (hw : c.S.names.contains ("d" ++ n) = false) (ht : c.S.names.contains "dt" = false)
    (rest : List Tok) (f : Nat) :
    pPrim c (f + 2) (.kw .frac :: .kw .lb :: .word ("d" ++ n) :: .kw .rb :: .kw .lb :: .word "dt" ::
      .kw .rb :: rest) = some (dNode (.str n) "t", rest)

\frac{dN}{dt} with an italic d, written as two words, reads as the time derivative of N when no variable d is declared and neither word is a declared name.

theorem variant_italic_d_sep (c : Ctx) (hc : c.sf = .latex) (n : String) (hn : nameOK n = true)
    (hd : c.S.names.contains "d" = false) (rest : List Tok) (f : Nat) :
    pPrim c (f + 2) (.kw .frac :: .kw .lb :: .letter 'd' :: (nameToks c n ++ .kw .rb :: .kw .lb ::
      .letter 'd' :: .letter 't' :: .kw .rb :: rest)) = some (dNode (.str n) "t", rest)

\frac{d N}{d t} with an italic d and N in its printed spelling reads as the time derivative of N, when no variable d is declared.

theorem variant_italic_d_typst (c : Ctx) (hc : c.sf = .typst) (n : String) (hn : nameOK n = true)
    (hd : c.S.names.contains "d" = false) (rest : List Tok) (f : Nat) :
    pPrim c (f + 1) (.kw .lpg :: .letter 'd' :: (nameToks c n ++ .kw .rp :: .kw .slash :: .kw .lpg ::
      .letter 'd' :: .letter 't' :: .kw .rp :: rest)) = some (dNode (.str n) "t", rest)

Typst (d N)/(d t) with an italic d reads as the time derivative of N, when no variable d is declared.

theorem variant_partial_t (c : Ctx) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 2) (.kw .frac :: .kw .lb :: .kw .pdiff :: ((pr c a).at c.sf 1 ++
      .kw .rb :: .kw .lb :: .kw .pdiff :: .letter 't' :: .kw .rb :: rest)) = some (dNode a "t", rest)

\frac{\partial N}{\partial t} reads as the time derivative of N, the same node as the canonical \frac{\mathrm{d} N}{\mathrm{d} t}.

theorem variant_partial_t_typst (c : Ctx) (hc : c.sf = .typst) (a : Json) (ha : M c a) (rest : List Tok)
    (f : Nat) (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 2) (.kw .lpg :: .kw .pdiff :: ((pr c a).at c.sf 1 ++
      .kw .rp :: .kw .slash :: .kw .lpg :: .kw .pdiff :: .letter 't' :: .kw .rp :: rest)) =
      some (dNode a "t", rest)

Typst (partial N)/(partial t) reads as the time derivative of N, the same node as the canonical (dif N)/(dif t).

theorem variant_italic_name (c : Ctx) (s : String) (rest : List Tok) (hr : Fol c.sf 10 rest) (f : Nat) :
    pPrim c (f + 1) (.it s :: rest) = some (.str s, rest)

\mathit{name} / italic("name") reads as the name, for any name (the explicit name shape), before anything that does not continue a name.

theorem variant_slash (c : Ctx) (hc : c.sf = .latex) (a b : Json) (ha : M c a) (hb : M c b)
    (rest : List Tok) (hr : Fol c.sf 5 rest) (f : Nat)
    (hf : need 6 ((pr c a).at c.sf 6).length + need 6 ((pr c b).at c.sf 6).length ≤ f) :
    pMul c (f + 2) ((pr c a).at c.sf 6 ++ .kw .slash :: ((pr c b).at c.sf 6 ++ rest)) =
      some (node "/" [a, b], rest)

An inline LaTeX a / b reads as the quotient node, the same node as the canonical \frac{a}{b}.

theorem variant_named_args (c : Ctx) (n : String) (bs : List (String × Json))
    (hn : tnameOK n = true) (hM : ∀ kv ∈ bs, M c kv.2) (hne : bs ≠ [])
    (hk : ∀ kv ∈ bs, nameOK kv.1 = true) (hnd : (bs.map Prod.fst).Nodup) (rest : List Tok) (f : Nat)
    (hf : need 10 (callToks c.sf [.opn n] (bs.map (itemToks c))).length ≤ f) :
    pPrim c f (callToks c.sf [.opn n] (bs.map (itemToks c)) ++ rest) =
      some (tNode n (sortKV bs), rest)

Named template arguments read as the template application, in any order (distinct names; the bindings are sorted to the printed order), and even when the symbol table knows the template’s parameters (the printer then writes them positionally).

theorem variant_euler_italic (c : Ctx) (hc : c.sf = .latex) (he : c.S.names.contains "e" = false)
    (a : Json) (ha : M c a) (rest : List Tok) (f : Nat) (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 3) (.letter 'e' :: .kw .caret :: .kw .lb :: ((pr c a).at c.sf 1 ++ .kw .rb :: rest)) =
      some (node "exp" [a], rest)

An italic e^{x} (LaTeX) reads as \exp(x) when no variable e is declared.

theorem variant_upright_e (r : List Char) :
    Typst.lexIdent ("upright(e)".toList ++ r) = some (.ups [("e", "")], r)

upright(e), unquoted, lexes to the token of upright("e").

theorem variant_euler_typst (c : Ctx) (hc : c.sf = .typst) (a : Json) (ha : M c a) (rest : List Tok) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 3) (.ups [("e", "")] :: .kw .caret :: .kw .lpg :: ((pr c a).at c.sf 1 ++ .kw .rp :: rest)) =
      some (node "exp" [a], rest)

Typst upright(e)^x and upright("e")^x read as exp(x), always (both lex to the token .ups [("e", "")], variant_upright_e ).

theorem variant_euler_italic_typst (c : Ctx) (hc : c.sf = .typst) (he : c.S.names.contains "e" = false)
    (a : Json) (ha : M c a) (rest : List Tok) (f : Nat) (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pPrim c (f + 3) (.letter 'e' :: .kw .caret :: .kw .lpg :: ((pr c a).at c.sf 1 ++ .kw .rp :: rest)) =
      some (node "exp" [a], rest)

Typst e^x with an italic e reads as exp(x) when no variable e is declared.

theorem refuse_removed_call (c : Ctx) (n : String) (hn : removedOps.contains n = true) :
    ∀ f ts, pOpn c f n ts = none

A removed operator is refused by name in the call form.

theorem refuse_removed_esc (c : Ctx) (o : String) (hn : removedOps.contains o = true) (f : Nat) (r : List Tok) :
    pPrim c (f + 1) (.esc o :: .kw .lb :: r) = none

A removed operator is refused by name in the LaTeX escape form.

theorem variant_native_call (c : Ctx) (n : String) (hcall : callOps.contains n = false)
    (hneg : n ≠ "neg") (hpow : n ≠ "pow") (hD : n ≠ "D") (hrem : removedOps.contains n = false)
    (ht : tparams c.S n = none) (f : Nat) (r : List Tok) (x : Json) (xs : List Json) (r' : List Tok)
    (ha : pCallArgs c f r = some ((x :: xs).map CallArg.pos, .kw .rp :: r')) :
    pOpn c (f + 1) n (.kw .lp :: r) = some (node n (x :: xs), r')

A native operator written in the call form, \operatorname{exp}(x) or op("exp")(x), reads as the native node exp(x): an operator name that is not a call-tier, deprecated, removed or template name reads as the node it names.