`if b then ... else ...` is never persistent
In some situations it is fairly natural to write a proposition as if b then P else Q
, where b: bool
. However, even if both P
and Q
are persistent, such a proposition cannot be moved into the persistent context, which can be somewhat annoying.
So I wonder, should we add instances for propositions defined via if
? Which typeclasses should get such instances? Is there some way we can make this work for all typeclasses in one go?