Re: [isabelle] Haskell code generation: Datatype Context



Hi Peter,

this question has been discussed in May on the developer list:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-May/002654.html

Florian then changed the code generator in changeset 1d11af40b106, which is after the Isabelle2012 release. So you can either patch your Isabelle2012 code or switch to the repository version.

Hope this helps,
Andreas

Am 29.08.2012 16:00, schrieb Peter Lammich:
Hi,

I tried to compile some code produced by the code generator with
ghc 7.4.1, and had to read the following error message:

     Illegal datatype context (use -XDatatypeContexts): Linorder a =>

When using the indicated compiler flag, it sais:

on the commandline:
     Warning: -XDatatypeContexts is deprecated: It was widely considered
a misfeature, and has been removed from the Haskell language.


So is there any easy way to get rid of that in the Haskell code
generator?


The error occured on this line, apparantly from RBT.thy:

newtype (Linorder a) =>  Rbt a b = Rbt (Rbta a b) deriving (Read, Show);


--
   Peter




--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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