Round trip, case by case: the escape form

Lean module Esm.Document.Math.Escape, formal/Esm/Document/Math/Escape.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases9

Every node has it: LaTeX \esm{op}{fields}{args} with the fields as JSON tokens, Typst esm.node("op", #(fields), args). The parser puts op and args back in their sorted places among the fields (mkNode_fieldsOf).

JSON tokens

Putting op and args back

theorem addAcc_of_lvl {c : Ctx} {kvs : List (String × Json)} (h : (pr c (.obj kvs)).lvl = 10) :
    addAcc (.obj kvs) = [.obj kvs]

The escape node

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