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 
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





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