Gergely Buday (Sep 14 2023 at 13:23): Gergely Buday (Sep 14 2023 at 13:23):In the theory Finite_Set, finite is a predicate on 'a set.
Is there a finite set type somewhere? I have heard that building a usable infrastructure with a typedef is much work and probably is not worth doing it.
Mathias Fleury (Sep 14 2023 at 13:27):https://isabelle.in.tum.de/library/HOL/HOL-Library/FSet.html
Mathias Fleury (Sep 14 2023 at 13:30):Though usually using the predicate is more than good enough…
Gergely Buday (Sep 14 2023 at 14:10):Are there set comprehensions for FSet?
Gergely Buday (Sep 14 2023 at 14:24):I solved this with ffold.
Wolfgang Jeltsch (Sep 14 2023 at 17:18):Gergely Buday said:
Are there set comprehensions for FSet?
I think they are, with a slightly different syntax to distinguish them from comprehensions for set. Best to check the source, which is online with syntax highlighting and hyperlinking.
Last updated: May 02 2024 at 08:19 UTC