Skip to content

Type classes for fancy updates and basic updates.

Jacques-Henri Jourdan requested to merge jh/bupd_fupd_classes into gen_proofmode

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.

Merge request reports