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

Christian Sternagel c-sterna at jaist.ac.jp
Sun Jun 24 08:02:21 CEST 2012

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



> 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

More information about the isabelle-dev mailing list