Commit 4e2b0860 by Robbert Krebbers

### Some tweaks.

 ... ... @@ -206,7 +206,7 @@ Ltac solve_to_val := match goal with | |- to_val ?e = Some ?v => let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v); apply W.to_val_Some; simpl; reflexivity apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity | |- is_Some (to_val ?e) => let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e'))); apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I ... ... @@ -227,7 +227,7 @@ Hint Extern 0 (language.atomic _) => solve_atomic : fsaV. (** Substitution *) Ltac simpl_subst := csimpl; simpl; repeat match goal with | |- context [subst ?x ?er ?e] => let er' := W.of_expr er in let e' := W.of_expr e in ... ...
 ... ... @@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp) : ⊢ WP rev hd acc {{ Φ }}. Proof. iIntros "(#Hh & Hxs & Hys & HΦ)". iLöb (hd acc xs ys Φ) as "IH". wp_rec; wp_let. iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let. destruct xs as [|x xs]; iSimplifyEq. - wp_match. by iApply "HΦ". - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!