Skip to content

Prove that invariants are "except 0".

Robbert Krebbersrequested to merge
robbert/inv_except_0 into master

This means you get things like ▷ False ⊢ inv N P, i.e., out of ▷ False you get any invariant.

Edited by Robbert Krebbers

Merge request reports