Re: [isabelle] Coinductive_List and LList/LFilter
On Thu, 2 Jul 2009, Andreas Lochbihler wrote:
there are two formalisations of coinductive lists in Isabelle/HOL 2009:
Library/Coinductive_List and Induct/LList, Induct/LFilter.
When I want to use coinductive lists, which one is recommended?
LList and LFilter go back to very early work by Larry Paulson from
1997/1998. There is some add-on material in AFP/Lazy-Lists-II based on
these theories. All of this is a bit dated.
Library/Coinductive_List is a renovated version of LList, although that is
already some years old now.
If you are serious about coinduction, you should try to port the old stuff
to make it work with Coinductive_List and submit the result to AFP. Then
we can delete the very old versions and future users won't get confused
This archive was generated by a fusion of
Pipermail (Mailman edition) and