kdrag.theories.set.Finite

kdrag.theories.set.Finite(A: ArrayRef) → BoolRef

A set is finite if it has a finite number of elements.

See: - https://cvc5.github.io/docs/cvc5-1.1.2/theories/sets-and-relations.html#finite-sets - https://isabelle.in.tum.de/library/HOL/HOL-Library/FSet.html

>>> IntSet = Set(smt.IntSort())
>>> kd.prove(Finite(IntSet.empty))
|= Exists(finwit!...,
       ForAll(x!...,
              K(Int, False)[x!...] ==
              Contains(finwit!..., Unit(x!...))))

Parameters:

A (ArrayRef)

Return type:

BoolRef