HOL4 defines llist's, potentially infinite lists. Is there an equivalent type operator in Isabelle/HOL?
Yes, in the Coinductive entry in the AFP: https://www.isa-afp.org/theories/coinductive/#Coinductive_List
Last updated: Apr 28 2024 at 01:11 UTC