Nathan Lutala (Dec 11 2023 at 08:21): Nathan Lutala (Dec 11 2023 at 08:21):Hello all,
I hope you're well. I had a small beginner question.
I'm currently learning a bit about the different data structures and types in Isabelle. I'm currently looking into lists. My question is, does the syntax below declare an empty list which can store any data type?
Hopefully, this makes sense. I really appreciate any help you can provide.
Yong Kiam (Dec 11 2023 at 08:34):not really, what you have written is a term, specifically applying the Cons constructor of the builtin list type on some term a and the empty list [], so it's really the singleton list [a] rather than the empty list
depending on what exactly you're trying to do (e.g., declare a new list type?) you may wish to check out: https://isabelle.in.tum.de/doc/prog-prove.pdf
Nathan Lutala (Dec 11 2023 at 08:53):Yong Kiam said:
not really, what you have written is a term, specifically applying the
Consconstructor of the builtin list type on some termaand the empty list[], so it's really the singleton list[a]rather than the empty listdepending on what exactly you're trying to do (e.g., declare a new list type?) you may wish to check out: https://isabelle.in.tum.de/doc/prog-prove.pdf
Oh ok, I get it now! Thanks for responding and for the link!
Last updated: Dec 21 2024 at 16:20 UTC