Commit b3bf8211 authored by Dan Frumin's avatar Dan Frumin

remove trailing whitespaces

parent 225b639d
......@@ -96,7 +96,7 @@ Definition dloc_var_of_dval (dv : dval) : option nat :=
Definition nat_of_dint (di : dint) : option (nat * option nat) :=
match di with
| dInt i None => guard (0 i); Some (Z.to_nat i, None)
| dInt i None => guard (0 i); Some (Z.to_nat i, None)
| dInt i (Some (IntNat j)) => guard (0 i); Some (Z.to_nat i, Some j)
| _ => None
end.
......@@ -176,7 +176,7 @@ Arguments dloc_var_interp !_ !_ /.
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
match dl with
| dLoc i dj =>
| dLoc i dj =>
match dint_interp' dj with
| Some j => dloc_var_interp E i + j
| None => dloc_var_interp E i
......
......@@ -417,14 +417,14 @@ Section denv.
Lemma denv_wf_dval_wf_lookup E i m q dv :
denv_lookup i m = Some (q, dv) denv_wf E m dval_wf E dv.
Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_dval_wf_delete_full_aux. Qed.
Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_dval_wf_delete_full_aux. Qed.
Lemma denv_wf_frac_wf_lookup E i m q dv :
denv_lookup i m = Some (q, dv) denv_wf E m (0 < q)%Q.
Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_frac_wf_delete_full_aux. Qed.
Proof. rewrite /denv_lookup; simplify; eauto using denv_wf_frac_wf_delete_full_aux. Qed.
Lemma denv_wf_delete_full E i m m' dv :
denv_delete_full i m = Some (m', dv) denv_wf E m denv_wf E m'.
Proof. rewrite /denv_delete_full; simplify; eauto using denv_wf_delete_full_aux. Qed.
Proof. rewrite /denv_delete_full; simplify; eauto using denv_wf_delete_full_aux. Qed.
Lemma denv_wf_dval_wf_delete_full E i m m' dv :
denv_delete_full i m = Some (m', dv) denv_wf E m dval_wf E dv.
Proof. rewrite /denv_delete_full; simplify; eauto using denv_wf_dval_wf_delete_full_aux. Qed.
......
......@@ -440,7 +440,7 @@ Section vcg_spec.
destruct de; simplify_eq/=; destruct_and?.
- (* return *)
destruct (dexpr_eval _) as [dv1|] eqn:?; simplify_eq /=; last first.
{ by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "$". }
{ by iDestruct (vcg_cwp_continuation_correct with "Hm H") as "$". }
iApply cwp_ret. iApply wp_wand; first by iApply dexpr_eval_correct.
iIntros (v ->). iApply (vcg_continuation_correct with "H"); eauto.
- (* bind *)
......
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