Re: [isabelle] Countable type: stream
> thank you Rene and Andreas for the help with the countable datatype, it works for a random type color.
> Now my last problem is to show that the datatype --- 'a stream --- is countable.
> Stream is a package in the FOCUS library and is smth defined with the HOLCF "domain" construct and resembles
> the lists in Haskell. To show now:
> instance stream :: (countable) countable
> by.... ?
> can you help me?
It definitely is not possible using the tactic mentioned by Andreas (which is based on
how "datatype"s are constructed by the datatype-package) and thus, also not by the wrapper
that makes use of this tactic in the "deriving" package.
So far I have never worked with HOLCF, but I just wondered whether you are sure that
stream really is countable: If it can model infinite lists (Haskell lists), then most
likely the set of all "bool stream"s already can encode the real interval [0,1] which is
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and