Commit c64b9a55 by Ralf Jung

### do not forget about sealing pvs and wp

parent 77a15fea
 ... @@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) => ... @@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) => | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega end; solve_validN. end; solve_validN. (* TODO: Consider sealing this, like all the definitions in upred.v. *) Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := {| uPred_holds n r1 := ∀ rf k Ef σ, {| uPred_holds n r1 := ∀ rf k Ef σ, 0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ → 0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ → ... ...
 ... @@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset) ... @@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset) wp_go (E ∪ Ef) (wp_pre E Φ) wp_go (E ∪ Ef) (wp_pre E Φ) (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) → (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) → wp_pre E Φ e1 n r1. wp_pre E Φ e1 n r1. (* TODO: Consider sealing this, like all the definitions in upred.v. *) Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ) Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}. (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}. Next Obligation. Next Obligation. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!