Round trip, case by case: fractions, powers, cases, initial conditions, indices, calls

Lean module Esm.Document.Math.Cases5, formal/Esm/Document/Math/Cases5.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases4

Lists

theorem pList_list proved source

theorem pList_list (c : Ctx) (closer : Tok) (hcl : ∀ r, Fol c.sf 1 (closer :: r))
    (hcc : closer ≠ .kw .comma)
    (hcl' : closer = .kw .rp ∨ closer = .kw .rpg ∨ closer = .kw .rb ∨ closer = .kw .rbk)
    (xs : List Json) (hx : ∀ x ∈ xs, M c x) (rest : List Tok) (f : Nat)
    (hf : need 1 (sepBy [.kw .comma] (xs.map fun x => (pr c x).at c.sf 1)).length + 3 ≤ f) :
    pList c f 1 (sepBy [.kw .comma] (xs.map fun x => (pr c x).at c.sf 1) ++ closer :: rest) =
      some (xs, closer :: rest)

A possibly empty comma list of children at level 1 before a closing token.

theorem pCallItems_list proved source

theorem pCallItems_list (c : Ctx) (closer : Tok) (hcl : ∀ r, Fol c.sf 4 (closer :: r))
    (hcc : closer ≠ .kw .comma) (hce : closer ≠ .kw .eq) :
    ∀ (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 4)).length + 2 ≤ f →
      pCallItems c f (sepBy [.kw .comma] (xs.map fun x => (pr c x).at c.sf 4) ++ closer :: rest) =
        some (xs.map CallArg.pos, closer :: rest)

Call arguments at level 4, positional.

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