Re: [isabelle] Countable type: stream

On Wed, May 29, 2013 at 3:16 AM, René Thiemann <rene.thiemann at> wrote:
>> instance stream :: (countable) countable
>> by.... ?
> 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
> uncountable.

René is right: The HOLCF stream type includes infinite lists and is
therefore uncountable (at least if the element type has cardinality >

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.