Esm.Units.Examples

Lean module Esm.Units.Examples, formal/Esm/Units/Examples.lean at 184aa13d35e5
Imports Esm.Units.GrammarLaws

Concrete checks of the §4.8.2 grammar on the spec’s own example strings (tests, not properties: the kernel evaluates normalisation, lexing and parsing).

def parseChars source

def parseChars (cs : List Char) : Except Err UExpr

Normalise, lex and parse (no table lookup).