[isabelle] Preservation of zeros in HOL/Tools/numeral_syntax.ML
I am presently hacking together a print translation so that words show
up in hexadecimal. I'm basing it on numeral_syntax.ML but there's
something I do not understand.
The comment at the top of numeral_syntax.ML says "preserves leading
zeros/ones". The code seems to support this claim, but where do these
zeros come from?
term "-0005 :: nat" gives "-5"
term "0005 :: nat" gives "5"
Basically, I'm wondering whether I should care about them or not.
This archive was generated by a fusion of
Pipermail (Mailman edition) and