Round trip, case by case: constant arrays

Lean module Esm.Document.Math.Arrays, formal/Esm/Document/Math/Arrays.lean at 184aa13d35e5
Imports Esm.Document.Math.Derivs

A column for rank 1 and a matrix of at least two columns, LaTeX bmatrix, Typst vec(…) / mat(…), with units after them as for a scalar.

def AOK source

def AOK : AForm → Prop

What a printed array shape guarantees.

theorem pPrim_arr proved source

theorem pPrim_arr (c : Ctx) (af : AForm) (haf : AOK af) (rest : List Tok) (f : Nat) :
    pPrim c (f + 1) (arrToks c.sf af ++ rest) = constTail af.json rest

The array tokens read back as the array, whatever follows them.

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