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: Jul 16 2026 at 21:01 UTC