Skip to content
Snippets Groups Projects
Commit c08bba36 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies; fix for `l ↦ -` removal

parent 769d2c32
No related branches found
No related tags found
No related merge requests found
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
"coq-iris" { (= "dev.2020-11-03.3.4cd21e62") | (= "dev") }
]
......@@ -193,7 +193,7 @@ Qed.
Lemma lapp_spec l1 l2 xs1 xs2 :
{{{ llist I l1 xs1 llist I l2 xs2 }}}
lapp #l1 #l2
{{{ RET #(); llist I l1 (xs1 ++ xs2) l2 - }}}.
{{{ RET #(); llist I l1 (xs1 ++ xs2) ( v, l2 v) }}}.
Proof.
iIntros (Φ) "[Hll1 Hll2] HΦ".
iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
......@@ -209,7 +209,7 @@ Qed.
Lemma lprep_spec l1 l2 xs1 xs2 :
{{{ llist I l1 xs2 llist I l2 xs1 }}}
lprep #l1 #l2
{{{ RET #(); llist I l1 (xs1 ++ xs2) l2 - }}}.
{{{ RET #(); llist I l1 (xs1 ++ xs2) ( v, l2 v) }}}.
Proof.
iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment