*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] nat_code Equation*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 4 Dec 2012 09:18:31 +0100*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <CAAMXsiYaGLygd6a_kE9efTsw_hd51nGjsjBpbCWsQMu56c5GgA@mail.gmail.com>*References*: <FB64BADF-227D-4ED8-988B-57680C25BB73@uibk.ac.at> <50B8CDE9.3070807@in.tum.de> <50B8D5FC.8040009@in.tum.de> <CAAMXsiagmLap6eB1tpjB8F-Lk3DV9jeZcxvbNRNcEbO1M7NVVQ@mail.gmail.com> <E23D8E77-94CA-4689-BA23-971780FC34DB@uibk.ac.at> <CAAMXsiYaGLygd6a_kE9efTsw_hd51nGjsjBpbCWsQMu56c5GgA@mail.gmail.com>

>> fun foo where >> "foo xs 0 = True" >> | "foo [] (Suc _) = False" >> | "foo (x # xs) (Suc n) = foo xs n" >> >> export_code foo in Haskell file - >> >> complains about >> >> "Nat.Suc" is not a constructor, on left hand side of equation, in theorem: >> foo [] (Suc ?uu) ≡ False > > The ML setup in Code_Nat.thy is intended to automatically translate > away patterns involving Suc, so that you don't have to do it yourself. > Unfortunately the translation is kind of picky; it only works if for > each rule with a "Suc n" pattern, there is a matching rule with a "0" > pattern in its place. I understand. > E.g. the following modification works with > Code_Nat.thy in Isabelle2012: > > fun foo where > "foo [] 0 = True" > | "foo (x # xs) 0 = True" > | "foo [] (Suc _) = False" > | "foo (x # xs) (Suc n) = foo xs n" > > But instead of changing your code, please try out the attached version > of Code_Nat.thy, where I have modified the code preprocessor. Thanks Brian, for the new version of Code_Nat. Unfortunately, it works for foo, but not for other functions. A minimized example that fails is as follows: fun double :: "nat ⇒ nat" where "double 0 = 0" | "double n = n + n" export_code double in Haskell file - Constructor as head in equation: nat_of_num ?n ≡ plus_nat_inst.plus_nat (pred_numeral ?n) (nat_of_num num.One) René

**Follow-Ups**:**Re: [isabelle] nat_code Equation***From:*Brian Huffman

**References**:**Re: [isabelle] nat_code Equation***From:*René Thiemann

**Re: [isabelle] nat_code Equation***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Indexed Sum/Product Operator
- Next by Date: Re: [isabelle] Indexed Sum/Product Operator
- Previous by Thread: Re: [isabelle] nat_code Equation
- Next by Thread: Re: [isabelle] nat_code Equation
- Cl-isabelle-users December 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