Skip to content
Snippets Groups Projects
Commit a98a72de authored by Ralf Jung's avatar Ralf Jung
Browse files

frame_and comment

parent e1aace82
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/class_instances_frame.v
+ 3
− 0
View file @ a98a72de
...@@ -106,6 +106,9 @@ Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R ...@@ -106,6 +106,9 @@ Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2. Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed. Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
(* For framing below [∧], we can frame [R] away in *both* conjuncts
(unlike with [∗] where we can only frame it in one conjunct).
We require at least one of those to make progress though. *)
Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' : Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
MaybeFrame p R P1 Q1 progress1 → MaybeFrame p R P1 Q1 progress1 →
MaybeFrame p R P2 Q2 progress2 → MaybeFrame p R P2 Q2 progress2 →
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment