From e108e63c5f3b13dd7242a4bfd077374344c64033 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?=
 <qcdz9r6wpcbh59@gmail.com>
Date: Wed, 6 Nov 2024 17:14:41 +0000
Subject: [PATCH] Add bindDispatch lemma for convenience

---
 theories/Imperative.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/Imperative.v b/theories/Imperative.v
index 97aecd6..3af1a2a 100644
--- a/theories/Imperative.v
+++ b/theories/Imperative.v
@@ -23,6 +23,9 @@ Fixpoint bind {effectType effectResponse A B} (a : Action effectType effectRespo
 
 Notation "x >>= f" := (bind x f) (at level 50, left associativity).
 
+Lemma bindDispatch {effectType effectResponse A B} effect (continuation : effectResponse effect -> Action effectType effectResponse A) (f : A -> Action effectType effectResponse B) : Dispatch _ _ _ effect continuation >>= f = Dispatch _ _ _ effect (fun response => continuation response >>= f).
+Proof. easy. Qed.
+
 Lemma leftIdentity {effectType effectResponse A B} (x : A) (f : A -> Action effectType effectResponse B) : bind (Done _ _ _ x) f = f x.
 Proof. easy. Qed.