Closed examples of the canonical unit spelling
Tests, not properties: the theorems quantifying over all inputs are in
Esm.Units.Canonical
and Esm.Units.Typeset
. Each example is checked by the kernel.
def factorsOf (s : String) : List Factor
The two-sided normal form of a unit string (empty when it does not parse).
Spellings that canonicalize alike
Rational exponents, %, kept symbols
No cancellation across the fraction bar
example : canon "bogus^0*s" = "bogus^0*s"
A dropped symbol must still name a unit: bogus does not, so the string is
left as written (and keeps failing to resolve).