Commit 2f224774 authored by Ralf Jung's avatar Ralf Jung
Browse files

exploit that fns return values

parent 15c4ca51
...@@ -52,7 +52,10 @@ Proof. ...@@ -52,7 +52,10 @@ Proof.
(* Call *) (* Call *)
sim_apply sim_simple_let_val=>/=. sim_apply sim_simple_let_val=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [done|done|solve_res|]. sim_apply (sim_simple_call 10 [] [] ε); [done|done|solve_res|].
intros rf frs frt FREL. intros rf frs frt _ _ _ _ FREL.
apply sim_simple_val. simpl.
sim_apply sim_simple_let_val=>/=.
(* Deref *)
Admitted. Admitted.
......
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