*To*: Steven Obua <obua at in.tum.de>*Subject*: Re: [isabelle] Numeral is acting strangely*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Tue, 04 Jul 2006 20:07:07 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <44AA36C3.3010907@in.tum.de>*References*: <44A8DB95.7010908@cse.unsw.edu.au> <44AA36C3.3010907@in.tum.de>*User-agent*: Thunderbird 1.5.0.4 (Windows/20060516)

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"

Cheers, Rafal Kolanski.

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

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

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

- 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