[isabelle] Preservation of zeros in HOL/Tools/numeral_syntax.ML

Hello Gentlemen,

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.


Rafal Kolanski.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.