[isabelle] Countable type: stream



Hello,


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.