Re: [isabelle] Countable type: stream



On Wed, May 29, 2013 at 3:16 AM, René Thiemann <rene.thiemann at uibk.ac.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 >
1).

- Brian




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