Round trip, case by case: expression templates

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

Positional arguments read back through the parameter list of the symbol table, and the parser sorts the bindings; named arguments read back in the printed (sorted) order.

Sorting bindings

Reserved names

Positional arguments

Named arguments

theorem pPrim_named proved source

theorem pPrim_named (c : Ctx) (n : String) (bs : List (String × Json))
    (hn : tnameOK n = true) (hM : ∀ kv ∈ bs, M c kv.2) (hne : bs ≠ [])
    (hk : ∀ kv ∈ bs, nameOK kv.1 = true) (hnd : (bs.map Prod.fst).Nodup) (rest : List Tok) (f : Nat)
    (hf : need 10 (callToks c.sf [.opn n] (bs.map (itemToks c))).length ≤ f) :
    pPrim c f (callToks c.sf [.opn n] (bs.map (itemToks c)) ++ rest) =
      some (tNode n (sortKV bs), rest)

Named template arguments, in any order and with distinct names, read back as the template application with its bindings sorted, whether or not the symbol table knows the template’s parameters (the printer writes them named, in sorted order, only when it does not; Esm.Document.Math.Variants.variant_named_args).

theorem sortKV_of_sorted proved source

theorem sortKV_of_sorted (bs : List (String × Json)) (hs : keysSorted bs = true) : sortKV bs = bs

Sorted bindings sort to themselves.

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