Commit 6fbbda09 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent 15ef2bba
......@@ -100,19 +100,17 @@ Section vcg.
λ v, ( E' dv m',
v = dval_interp E' dv
E `prefix_of` E'
(denv_wf E' m')
denv_wf E' m'
dval_wf E' dv
denv_interp E' m'
(Φ E' m' dv))%I.
Φ E' m' dv)%I.
Arguments vcg_wp_postcondition : simpl never.
Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m (awp (dcexpr_interp E de) R (vcg_wp_postcondition E Φ)).
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : denv dval iProp Σ) : iProp Σ :=
match is_dloc E dv with
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