Re: [isabelle] Haskell code generation: Datatype Context

Hi Peter,

this question has been discussed in May on the developer list:

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,

Am 29.08.2012 16:00, schrieb Peter Lammich:

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

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

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


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 - 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.