Round trip, case by case: literals, prefix and infix operators

Lean module Esm.Document.Math.Cases3, formal/Esm/Document/Math/Cases3.lean at 184aa13d35e5
Imports Esm.Document.Math.Loops

theorem grp_child proved source

theorem grp_child {c : Ctx} {a : Json} (ha : M c a) (L : Nat) (h1 : 1 ≤ L) (h10 : L ≤ 10)
    (rest : List Tok) (hr : Fol c.sf L rest) (f : Nat)
    (hf : need L ((pr c a).toks.length + 2) ≤ f) :
    pLvl c f L (grp c.sf (pr c a).toks ++ rest) = some (a, rest)

A child in parentheses reads back at any level.

def sepBlocks source

def sepBlocks (sep : Tok) (c : Ctx) (L : Nat) (ys : List Json) : List (Json × List Tok)

The blocks after the first operand of a chain with a separator token.

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