From 48de4691fc646af15a14946e130b696bec6ce688 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Sun, 28 Jan 2024 22:08:38 +0100
Subject: [PATCH] Basic tactic support for resolving new_chan
---
theories/channel/proofmode.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 0d000fe..71c8b53 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -484,3 +484,8 @@ Tactic Notation "wp_select" "with" constr(pat) :=
end.
Tactic Notation "wp_select" := wp_select with "[//]".
+
+Tactic Notation "wp_new_chan" constr(prot) "as"
+ "(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
+ wp_smart_apply (new_chan_spec prot); [done|];
+ iIntros (c1); iIntros (c2); iIntros pat.
--
GitLab