Round trip, case by case: open operators

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

theorem jsonVal_head proved source

theorem jsonVal_head (sf : Sf) (v : Json) (hv : jwf v = true) (hn : isE v = false) :
    ∃ t r, jsonVal sf v = t :: r ∧
      (sf = .latex → ∀ X, jsonStart (t :: X) = true) ∧ (sf = .typst → t = .code v ∧ r = [])

A field value as JSON tokens starts with a token the parser takes for JSON.

def valToks source

def valToks (c : Ctx) (v : Json) : List Tok

A field value as printed: an expression at level 4, or JSON.

def fieldToks source

def fieldToks (c : Ctx) (kv : String × Json) : List Tok

A field as printed: key, =, value.

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