Commit 8705dec5 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Blah.

parent 25d92348
......@@ -244,7 +244,7 @@ Proof using.
xletfun => F HF.
ram_apply_let (rule_box_up2 (fun (x:int) => (x + n)%Z) n).
{ intros. xdef. xletapp rule_box_get => m ->.
ram_apply rule_add. { auto with iFrame. } } (* TODO : improve. *)
ram_apply rule_add. { auto with iFrame. } }
{ iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
auto with iFrame. }
unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
......
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