[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?

Many thanks!


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