The LaTeX math round trip, at the string level

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

def printLatex source

def printLatex (S : Sym) (e : Json) : String

The LaTeX math spelling of an expression under the symbol table S.

def parseLatex source

def parseLatex (S : Sym) (s : String) : Option Json

Read LaTeX math under the symbol table S.

theorem parseLatex_printLatex proved source

theorem parseLatex_printLatex (S : Sym) (e : Json) (he : isE e = true) :
    parseLatex S (printLatex S e) = some e

The LaTeX round trip: every well-formed expression reads back from its LaTeX spelling, under every symbol table (collisions included: the printer switches the names involved to the explicit form).