Stream: Beginner Questions

Topic: Potentially infinite lists

view this post on Zulip Gergely Buday (Apr 13 2023 at 15:17):

HOL4 defines llist's, potentially infinite lists. Is there an equivalent type operator in Isabelle/HOL?

view this post on Zulip Dmitriy Traytel (Apr 13 2023 at 15:41):

Yes, in the Coinductive entry in the AFP: https://www.isa-afp.org/theories/coinductive/#Coinductive_List

Last updated: May 31 2025 at 04:25 UTC