Stream: Beginner Questions

Topic: Potentially infinite lists

Gergely Buday (Apr 13 2023 at 15:17):

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

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: Dec 08 2025 at 08:34 UTC