The LaTeX printer writes only LaTeX tokens

Lean module Esm.Document.Math.TokLatex, formal/Esm/Document/Math/TokLatex.lean at 184aa13d35e5
Imports Esm.Document.Math.LexLatex

Every token of a printed well-formed expression is a LaTeX token (tokOK ), so the LaTeX lexer lemma applies to the printer’s output.

macro "aok" : tactic

Close a goal AllOK [fixed tokens and pieces] from the pieces in the context.

Names

theorem print_tokOK proved source

theorem print_tokOK (S : Sym) (e : Json) (he : isE e = true) : ∀ t ∈ print .latex S e, tokOK t

Every token the LaTeX printer writes for a well-formed expression is a LaTeX token.

This module also proves 34 lemmas without doc comments; they are in the source.