The Typst math round trip, at the string level

Lean module Esm.Document.Math.RoundTripTypst, formal/Esm/Document/Math/RoundTripTypst.lean at 184aa13d35e5
Imports Esm.Document.Math.TokTypst

def printTypst source

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

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

def parseTypst source

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

Read Typst math under the symbol table S.

theorem parseTypst_printTypst proved source

theorem parseTypst_printTypst (S : Sym) (e : Json) (he : isE e = true) :
    parseTypst S (printTypst S e) = some e

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