*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Efficient Integers?*From*: Thomas Genet <Thomas.Genet at irisa.fr>*Date*: Fri, 10 Feb 2012 10:01:55 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F34DB4C.8080206@in.tum.de>*References*: <4F34D68F.1070409@irisa.fr> <4F34DB4C.8080206@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.5; rv:10.0) Gecko/20120129 Thunderbird/10.0

Le 10/02/12 09:54, Tobias Nipkow a écrit :

PS No, you don't get machine integers, that would be unsound. You get big integers, which are language specific. I assume that in most of the languages we support big integers are like machine integers plus some fixed overhead, as long as you stay in the machine integer range.

Thanks a lot Tobias, this is even better that what I expected! Thomas -- Thomas Genet ISTIC/IRISA Campus de Beaulieu, 35042 Rennes cedex, France Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr http://www.irisa.fr/celtique/genet

**References**:**[isabelle] Efficient Integers?***From:*Thomas Genet

**Re: [isabelle] Efficient Integers?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Efficient Integers?
- Next by Date: [isabelle] 2 new AFP entries
- Previous by Thread: Re: [isabelle] Efficient Integers?
- Next by Thread: Re: [isabelle] Efficient Integers?
- Cl-isabelle-users February 2012 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