Type classes for fancy updates and basic updates.
The typeclasses are called BUpd
and FUpd
. The instances for upred are called uPred_fupd
and uPred_bupd
. Lemma about uPred_bupd
are called uPred_bupd_xxx
while lemmas about uPred_fupd
are called fupd_xxx
. This is inconsistent: should we rename fupd
lemmas?
I'd like to define instances for monPred. However, if I do that in monpred.v
, then monPred.v
will depend on things in base_logic/
, which is not ideal. On the other hand, adding these instances where the class is define would make uPred definition depend on monPred, which is meaningless.
An alternative is to define these classes in interface.v
, but this has little to do with what BIs are.