Re: [isabelle] Customise the Haskell code generator?

Dear Florian,

first of all, thanks for the awesome work on the code generator!

2016-08-04 9:23 GMT+02:00 Florian Haftmann <
florian.haftmann at>:
> Hi Moa,
> Am 03.08.2016 um 12:59 schrieb Moa Johansson:
> > Hi!
> >
> > Iâm wondering if itâs possible to customise the Haskell code generator:
A normal user probably want it to translate e.g. various list functions to
the corresponding Haskell library functions. However, in our application it
would make our lives slightly easier if we had the option to also include
those (library) function definitions explicitly in the resulting .hs file,
instead of creating a file that imports them. So just wanted to check if
this is possible somehow, to maybe save myself some work.
> you can reset those target language specific adaptations using
> Âcode_printingÂ, e.g.
> code_printing
>   constant append â (Haskell)
> export_code append in Haskell
> See the Isar Reference Manual and the Tutorial on Code Generation for
> details.

Similar to <import "~~/src/HOL/Library/Code_Target_Int">, is there
something like
<import "~~/src/HOL/Library/Code_Trust_the_Target_Language_Standard_Library">?


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