Re: [isabelle] Numeral is acting strangely




Steven Obua wrote:
actually, in general "Numeral0::'a" is NOT equal to "0::'a".

I figured that out. What I can't figure out is why

term "0" is	"0::'a" :: "'a"
term "1" is	"1::'a" :: "'a"
term "2" is	"2::'a" :: "'a"

but

term "00" is	"Numeral0" :: "'a"
term "01" is	"Numeral1" :: "'a"
term "02" is	"2::'a" :: "'a"

Does that make any sense to you? 00 is intuitively just 0, just like 01 is 1. Instead we get "Numeral0" and "Numeral1", but for 02 we get "2".

In the hex input modification, I want 0x0 to be 0, and 0x1 to be 1. I'm already getting 0x2 to be 2.

Larry Paulson already indicated that 0 and 1 are "special", but it isn't clear to me how it applies to this case. Does isabelle actually single out 1 and 0 before we get to the functions in HOL/Tools/numeral_syntax.ML?

Cheers,

Rafal Kolanski.





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