Skip to content

Restructure derived_laws of BI

Robbert Krebbers requested to merge robbert/restructure_bi into master

Some changes in preparation of !881 (merged)

  • Move pure lemmas down; that is already in !881 (merged)
  • Move Affine/Absorbing/Persistent instances up to fix some of the TODOs there (and some other circular issues that I have in my extension of !881 (merged)).

This MR should not add/remove/change any lemma statements. I changed some proofs to make things work with the new order.

Merge request reports