• Robbert Krebbers's avatar
    Some refactoring of the proofmode proofs. · 2cec343c
    Robbert Krebbers authored
    I have introduced the following definition to avoid many case
    analyses where both branches had nearly identical proofs.
    
    Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
      (if p then □ P else P)%I.
    2cec343c
pviewshifts.v 8.57 KB