Names read back

Lean module Esm.Document.Math.Names, formal/Esm/Document/Math/Names.lean at 184aa13d35e5
Imports Esm.Document.Math.View

pName_nameToks : the tokens of a name read back to the name, whatever symbol table printed them, before anything that does not continue a name (NameStop : not the scope dot, not an upright name subscript).

Splitting at dots

theorem splitDots_noDot proved source

theorem splitDots_noDot (l : List Char) : ∀ s ∈ splitDots l, '.' ∉ s

Every segment of a split has no dot.

Segments

def NameStop source

def NameStop (sf : Sf) (rest : List Tok) : Prop

What may follow a name: not the scope dot, not an upright name subscript.

theorem pName_nameToks proved source

theorem pName_nameToks (c : Ctx) (s : String) (hs : nameOK s = true) (rest : List Tok)
    (hr : NameStop c.sf rest) : pName c.sf (nameToks c s ++ rest) = some (s, rest)

Names read back.

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