Commit b8dc1d84 authored by Robbert Krebbers's avatar Robbert Krebbers

Version of wp_bind_inv for ectx languages.

Typeclass search gets less confused when this version is used, also,
we had the same for `wp_bind` already.
parent 12f8178f
......@@ -16,6 +16,10 @@ Lemma wp_ectx_bind {E Φ} K e :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_ectx_bind_inv {E Φ} K e :
WP fill K e @ E {{ Φ }} WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
Proof. apply: weakestpre.wp_bind_inv. Qed.
Lemma wp_lift_head_step {E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
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