The Typst printer writes only Typst tokens, in lexable order
Every token of a printed well-formed expression is a Typst token (tokOK
), every call
parenthesis follows a name-like token, and no unit block follows a unit block
(Adj
), so the Typst lexer lemma applies to the printer’s output.
def Nice (ts : List Tok) : Prop
A list that may follow anything: it does not start with a call parenthesis or a unit block.
macro "gok" : tactic
Close Good, Nice
and fact goals about a printed template from the pieces in
the context.
Names
Printer pieces
Reductions
The induction
theorem print_ok (S : Sym) (e : Json) (he : isE e = true) :
(∀ t ∈ print .typst S e, tokOK t) ∧ Adj (print .typst S e) ∧ ∀ r, print .typst S e ≠ .kw .lp :: r
Every token the Typst printer writes for a well-formed expression is a Typst token, in an order the Typst lexer reads back.