*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Wed, 03 Jul 2013 23:46:12 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51D4A7E7.1000109@in.tum.de>*Organization*: University of Birmingham*References*: <51D3205A.5030303@gmail.com> <51D46E5F.7000804@informatik.tu-muenchen.de> <51D49B99.20408@gmail.com> <51D4A7E7.1000109@in.tum.de>*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130627 Thunderbird/17.0.7

2013-07-03 23:38 Manuel Eberl: > On 07/03/2013 11:46 PM, Christoph LANGE wrote: >> I am nowhere near an _experienced_ Scala programmer yet, but >> sufficiently capable of writing wrapper functions that, e.g., convert >> set[Nat] to List[Int] […] > > At the danger of being called a nitpicker: this sort of thing can cost > you the programme correctness that you have so painstakingly ensured > with Isabelle, since Int in Scala is subject to integer overflow. > … > Personally, unless I do some heavy number-crunching, I use the > arbitrary-precision Integer type (in Haskell) just to be sure – > especially with Isabelle-generated code. Thanks for pointing out. Indeed BigInt would be the right type to use in Scala. Cheers, Christoph -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Intelligent Computer Mathematics, 8–12 July, Bath, UK. http://cicm-conference.org/2013/ → Modular Ontologies (WoMO), 15 September, Corunna, Spain. Submission until 12 July; http://www.iaoa.org/womo/2013.html → Knowledge and Experience Management, 7-9 October, Bamberg, Germany. Submission until 15 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/ → Mathematics in Computer Science Special Issue on “Enabling Domain Experts to use Formalised Reasoning”; submission until 31 October. http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

**References**:**[isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Christoph LANGE

**Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Florian Haftmann

**Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Christoph LANGE

**Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Date: [isabelle] prove simple inequality
- Previous by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Cl-isabelle-users July 2013 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