*To*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problems with Code-Generator*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 30 Sep 2016 10:05:11 +0200*In-reply-to*: <13F3E45C-B507-479E-B5DB-F470ECD384A6@uibk.ac.at>*References*: <13F3E45C-B507-479E-B5DB-F470ECD384A6@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Dear RenÃ,

One could try to come up with a better implementation, but it's not that easy. Best, Andreas On 30/09/16 09:47, Thiemann, Rene wrote:

Dear list, we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers. theory Test imports Main "~~/src/HOL/Library/Code_Target_Numeral" begin fun foo :: "nat â bool" where "foo (Suc 0) = True" export_code foo in Haskell (* "Nat.Suc" is not a constructor, on left hand side of equation, in theorem: foo (Suc zero_nat_inst.zero_nat) â True *) end Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future. The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71. Cheers, Akihisa and RenÃ

**Follow-Ups**:**Re: [isabelle] Problems with Code-Generator***From:*Thiemann, Rene

**References**:**[isabelle] Problems with Code-Generator***From:*Thiemann, Rene

- Previous by Date: [isabelle] Problems with Code-Generator
- Next by Date: [isabelle] pairs and friends
- Previous by Thread: [isabelle] Problems with Code-Generator
- Next by Thread: Re: [isabelle] Problems with Code-Generator
- Cl-isabelle-users September 2016 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