Round trip of the atoms: numbers and names

Lean module Esm.Document.Math.Atoms, formal/Esm/Document/Math/Atoms.lean at 184aa13d35e5
Imports Esm.Document.Math.Kinds

def SegHead source

def SegHead (g : List Char) (t : Tok) (tr : List Tok) : Prop

How a printed name segment starts.

def NameHead source

def NameHead (c : Ctx) (s : String) (t : Tok) (tr : List Tok) : Prop

How a printed name starts.

theorem pPrim_name_eq proved source

theorem pPrim_name_eq (c : Ctx) (s : String) (rest : List Tok) (f : Nat) :
    pPrim c (f + 1) (nameToks c s ++ rest) = pNamePrim c (nameToks c s ++ rest)

A primary that starts with a name’s tokens is read as a name (never as e^x).

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