Find better place for pred_finite and pred_infinite
std++ not only has typeclasses for Finite T
and Infinite T
on the type level (defined in finite.v
and infinite.v
); it also has notions of when a predicate (viewed as a "propset") is finite or infinite: pred_finite
and pred_infinite
are defined in sets.v
. However, that file really seems like the wrong place for these definitions.
I see two options here:
- We move them to
propset.v
. However, whileT → Prop
is isomorphic to propsets,pred_finite
andpred_infinite
don't actually use the propset type (and changing them to use that would be annoying for the way we use these notions in Iris), so this is stretching things a bit. - We move them to
finite.v
andinfinite.v
. However, then where do we put the one lemma that involves both notions:pred_infinite P → pred_finite P → False
?