*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Numeral is acting strangely*From*: Steven Obua <obua at in.tum.de>*Date*: Tue, 04 Jul 2006 12:26:06 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <44AA3DCB.5040401@cse.unsw.edu.au>*References*: <44A8DB95.7010908@cse.unsw.edu.au> <44AA36C3.3010907@in.tum.de> <44AA3DCB.5040401@cse.unsw.edu.au>*User-agent*: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.3) Gecko/20040915

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 like01 is 1. Instead we get "Numeral0" and "Numeral1", but for 02 we get "2".

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 itisn't clear to me how it applies to this case. Does isabelle actuallysingle out 1 and 0 before we get to the functions inHOL/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

**Follow-Ups**:**Re: [isabelle] Numeral is acting strangely***From:*Rafal Kolanski

**References**:**[isabelle] Numeral is acting strangely***From:*Rafal Kolanski

**Re: [isabelle] Numeral is acting strangely***From:*Steven Obua

**Re: [isabelle] Numeral is acting strangely***From:*Rafal Kolanski

- Previous by Date: Re: [isabelle] Numeral is acting strangely
- Next by Date: Re: [isabelle] Numeral is acting strangely
- Previous by Thread: Re: [isabelle] Numeral is acting strangely
- Next by Thread: Re: [isabelle] Numeral is acting strangely
- Cl-isabelle-users July 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list