[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
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