[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

Tobias Nipkow nipkow at in.tum.de
Tue May 8 16:09:15 CEST 2012

Am 08/05/2012 13:49, schrieb Peter Lammich:
> datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"

Actually, I think this does not do what you hope it does, hence the magic is
still in there. But Lukas showed me a related defn:

datatype 'a ref = Ref nat

where 'a is a phantom type but for extra-logical reasons you want to restrict 'a
to some type class. Extra-logical reasons can be quite compelling ;-) I'm convinced.


More information about the isabelle-dev mailing list