Re: [isabelle] Preservation of zeros in HOL/Tools/numeral_syntax.ML
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and