[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
can you help me?
This archive was generated by a fusion of
Pipermail (Mailman edition) and