Type class for finitely enumerable types. The property is stronger
than Fintype
in that it assigns each element a rank in a finite
enumeration.
- card : ℕ
FinEnum.card
is the cardinality of theFinEnum
- equiv : α ≃ Fin (FinEnum.card α)
- decEq : DecidableEq α
FinEnum α
means that α
is finite and can be enumerated in some order,
i.e. α
has an explicit bijection with Fin n
for some n.
Instances
create a FinEnum
instance from an exhaustive list without duplicates
Instances For
create a FinEnum
instance from an exhaustive list; duplicates are removed
Instances For
create an exhaustive list of the values of a given type
Instances For
create a FinEnum
instance using a surjection
Instances For
create a FinEnum
instance using an injection
Instances For
enumerate all finite sets of a given type
Equations
- FinEnum.Finset.enum [] = [∅]
- FinEnum.Finset.enum (x_1 :: xs) = do let r ← FinEnum.Finset.enum xs [r, {x_1} ∪ r]
Instances For
For Pi.cons x xs y f
create a function where every i ∈ xs
is mapped to f i
and
x
is mapped to y
Instances For
pi xs f
creates the list of functions g
such that, for x ∈ xs
, g x ∈ f x
Equations
- FinEnum.pi [] x = [fun x h => False.elim (_ : False)]
- FinEnum.pi (x_2 :: xs) x = Seq.seq (FinEnum.Pi.cons x_2 xs <$> x x_2) fun x => FinEnum.pi xs x