[isabelle-dev] [isabelle] codatatypes (was "Formalisations of infinite streams" on isabelle-users)

[Christian Sternagel]

Dear all,

I was wondering, what's the status of the codatatype package? And will 
it be an official Isabelle/HOL package? Will there be Haskell 
code-generation for (functions on) codatatypes?)

cheers

chris

> Hi Andreas,
>
> some thoughts here from Munich:
> - Having dedicated type "'a stream" for functions (nat => 'a) has
> similar benefits and drawbacks as the set/'a => bool distinction.  Alex
> Krauss sent a nice summary (Summary: WHY have 'a set back?) on
> isabelle-dev about a year ago. Creating a new type has been recently
> simplified by the lift_definition command and transfer method.
>
> - Dmitriy Traytel and Andrej Popescu are developing a codatatype
> package, which might be useful for your work. (The package will be done
> in "two weeks".)
>
> Lukas
>
>