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 again.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.