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.

https://isabelle.in.tum.de/library/HOL/HOL-Library/FSet.html

Though usually using the predicate is more than good enough…

Are there set comprehensions for FSet?

I solved this with ffold.

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: Dec 07 2023 at 08:19 UTC