Skip to content
Snippets Groups Projects
Commit dfef4e62 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Improved fork_chan proofmode

parent d36fe30f
No related branches found
No related tags found
No related merge requests found
Pipeline #96064 passed
Hide whitespace changes
Inline Side-by-side
theories/channel/proofmode.v
+ 8
− 3
View file @ dfef4e62
......@@ -491,10 +491,15 @@ Tactic Notation "wp_new_chan" constr(prot) "as"
iIntros (c1); iIntros (c2); iIntros pat.
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c1) constr(pat1) "and" simple_intropattern(c2) constr(pat2) :=
simple_intropattern(c1) constr(pat1) "and"
simple_intropattern(c2) constr(pat2) :=
wp_smart_apply (fork_chan_spec prot); [iIntros (c2); iIntros pat2|
iIntros (c1); iIntros pat1].
Tactic Notation "wp_fork_chan" constr(prot) :=
wp_smart_apply (fork_chan_spec prot).
Tactic Notation "wp_fork_chan" constr(prot) "as"
simple_intropattern(c) constr(pat) :=
wp_fork_chan prot as c pat and c pat.
Tactic Notation "wp_fork_chan" constr(prot) :=
let iNew := iFresh in
wp_fork_chan prot as ? iNew.
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