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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
