# Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*