Commit aec84909 authored by Robbert Krebbers's avatar Robbert Krebbers

Make argument K of wp_bind explicit.

parent 5e72fb3f
Pipeline #2894 passed with stage
in 9 minutes and 22 seconds
......@@ -145,7 +145,7 @@ Proof.
iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
......
Markdown is supported
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