Skip to content
GitLab

Prove that invariants are "except 0".

Merged Robbert Krebbers requested 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