Commit 3b0c15c3 by Robbert Krebbers

### Use normal function arrow → for `saved_pred_own`.

parent 2a1af810
 ... ... @@ -90,19 +90,20 @@ Qed. Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)). Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)). Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -c> iProp Σ) := Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) := saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ). Proof. solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]). Qed. Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -c> iProp Σ) : Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) : (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I. Proof. iApply saved_anything_alloc_strong. Qed. Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A -c> iProp Σ) : Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) : (|==> ∃ γ, saved_pred_own γ Φ)%I. Proof. iApply saved_anything_alloc. Qed. ... ...
Supports Markdown
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