# Re: [isabelle] Numeral is acting strangely

```Rafal Kolanski wrote:

```
```
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".
```
```
As Larry already pointed out, "0" and "1" are actually declared global constants (see HOL.thy in the isabelle/src/HOL directory), while "2", "3" and so on are not. Therefore the parser recognizes these global constants first. "00" is not a declared constant, therefore it is passed on to the functions in numeral_syntax.ML. So to me it makes perfect sense (it may not be intuitive, though :-)).
```
```
"2::'a" is just a pretty-printed version of a more complex term. You cannot pretty-print "Numeral0" in that way, because then "Numeral0" would have to become "0", but as you already figured out, "Numeral0" is not the same as "0", therefore this pretty-printing would be maybe intuitive, but wrong.
```
Steven

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

```
```

--
Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
Raum: 01.11.059

```

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