Email Gateway (Aug 19 2022 at 08:26): Email Gateway (Aug 19 2022 at 08:26):From: Peter Lammich <lammich@in.tum.de>
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);
Email Gateway (Aug 19 2022 at 08:26):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Last updated: Apr 19 2024 at 16:20 UTC