Email Gateway (Aug 18 2022 at 11:36): Email Gateway (Aug 18 2022 at 11:36):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 11:37):From: Makarius <makarius@sketis.net>
On Fri, 28 Mar 2008, Rafal Kolanski wrote:
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"
This is just the usual situation that the comment disagrees with the ML
text. In the present version leading zeros are stripped from the input,
but are printed if they are produced internally (e.g. by logical
transformations).
Numerals have many more problems, such as the builtin sign. What
Basically, I'm wondering whether I should care about them or not.
It depends what exactly you have in mind. You could just mimic the
present behaviour, or try to do better, e.g. by not printing terms with
leading zeros as numerals.
Makarius
Last updated: May 03 2024 at 12:27 UTC