Commit 85997565 authored by Dan Frumin's avatar Dan Frumin

Forgot binop.v lol

parent 782c4829
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section test.
Context `{amonadG Σ}.
Lemma ptr_plus_test1 (p q : cloc) (n : nat) v1 R Φ :
Φ (cloc_to_val (cloc_plus p n)) -
p C v1 -
q C cloc_to_val p -
AWP (∗ᶜ♯ₗq +∗ᶜ n) @ R {{ v, Φ v p C v1 q C cloc_to_val p }}.
Proof.
iIntros "HΦ Hp Hq". vcg_solver.
rewrite Qp_half_half.
eauto with iFrame.
Qed.
End test.
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