[isabelle] Customise the Haskell code generator?


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.

I currently generate the code using the function Code_Target.export_code, which takes many arguments but it wasnât obvious if any of them control what I want to do.


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