*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation*From*: Aaron Gray <aaronngray.lists at gmail.com>*Date*: Fri, 7 Dec 2012 23:54:02 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <E264DDCD-1B6B-4B32-80EC-B621F7D9D3BE@uibk.ac.at>*References*: <CANkmNDdVzsLAQZPQtpcKrXGuiRBP_dAnA=f6dWE4Bretmpqnig@mail.gmail.com> <E264DDCD-1B6B-4B32-80EC-B621F7D9D3BE@uibk.ac.at>

Dear René, Thanks for the info and tips. Hopefully I will get somewhere tomorrow. Regards, Aaron On 7 December 2012 11:52, René Thiemann <rene.thiemann at uibk.ac.at> wrote: > Dear Aaron, > > > How do I generate Haskell and ML and friends from a proof like CoreC++ > for > > example ? > > As far as I know, you cannot generate Haskell code from a "proof", but > just from > definitions and functions, and in certain cases also from inductive > definitions > by using the predicate compiler. > > In principle, everything that can be written as an equality "lhs = rhs" > can be fed > to the code-generator. > > lemma [code]: "lhs = rhs" > proof ... > > declare my_theorem[code] > > then getting the code is as easy as writing > > export_code some_function in Haskell file ... > > however, it might fail whenever there are non-executable involved. > > For example, defining > > definition fermat where "fermat n = (?x y z. x > 0 /\ y > 0 /\ x^n + y^n = > z^n)" > > then > > export_code fermat in Haskell file - > > will fail, but if you first prove a code-equation > > lemma fermat_code[code]: "fermat n = (n <= 2)" > proof ... > > then of course it will become executable. > > Further information on the code-generator can be found by > > isabelle doc codegen > > Hope this helps, > René > -- > René Thiemann mailto:rene.thiemann at uibk.ac.at > Computational Logic Group > http://cl-informatik.uibk.ac.at/~thiemann/ > Institute of Computer Science phone: +43 512 507-6434 > University of Innsbruck > >

**References**:**[isabelle] newbie questions r.e. Isar to Haskell/ML generation***From:*Aaron Gray

**Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation***From:*René Thiemann

- Previous by Date: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- Next by Date: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- Previous by Thread: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- Next by Thread: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- 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