Round trip, case by case: atoms, prefix operators, functions

Lean module Esm.Document.Math.Cases1, formal/Esm/Document/Math/Cases1.lean at 184aa13d35e5
Imports Esm.Document.Math.Main

theorem child1 proved source

theorem child1 {c : Ctx} {a : Json} (h : M c a) (rest : List Tok) (hr : Fol c.sf 1 rest) (f : Nat)
    (hf : need 1 ((pr c a).at c.sf 1).length ≤ f) :
    pOr c f ((pr c a).at c.sf 1 ++ rest) = some (a, rest)

A child’s tokens for level 1 read back before a closing token.

theorem pItems_list proved source

theorem pItems_list (c : Ctx) (L : Nat) (hL : L = 1 ∨ L = 4) (closer : Tok)
    (hcl : ∀ r, Fol c.sf L (closer :: r)) (hcc : closer ≠ .kw .comma) :
    ∀ (xs : List Json), xs ≠ [] → (∀ x ∈ xs, M c x) → ∀ rest f,
      need 1 (sepBy [.kw .comma] (xs.map fun x => (pr c x).at c.sf L)).length + 2 ≤ f →
      pItems c f L (sepBy [.kw .comma] (xs.map fun x => (pr c x).at c.sf L) ++ closer :: rest) =
        some (xs, closer :: rest)

A comma-separated list of printed expressions at level L reads back.

Assembling the induction facts

theorem M_of proved source

theorem M_of (c : Ctx) (e : Json) (h0 : P0 c e) (hh : HeadOK c (pr c e).toks)
    (hl1 : 1 ≤ (pr c e).lvl) (hl : (pr c e).lvl ≤ 10) (hlvl : (pr c e).lvl ≠ 4)
    (hacc : addAcc e = [e]) (hcrow : (pr c e).crow = (pr c e).toks ++ [.kw .amp, .txt "otherwise"]) :
    M c e

The facts for an expression printed with the generic crow and not a + chain.

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