From 9f0e4605e1c8816dbf5ed3e9e893b25e9a2be4a3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 26 Jan 2024 00:17:59 +0100
Subject: Improve the Lean backend

---
 backends/lean/Base/Primitives/Base.lean | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'backends/lean/Base/Primitives/Base.lean')

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 3d70c84a..9dbaf133 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -116,6 +116,13 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
 @[simp] theorem bind_tc_div (f : α → Result β) :
   (do let y ← div; f y) = div := by simp [Bind.bind, bind]
 
+@[simp] theorem bind_assoc_eq {a b c : Type u}
+  (e : Result a) (g :  a → Result b) (h : b → Result c) :
+  (Bind.bind (Bind.bind e g) h) =
+  (Bind.bind e (λ x => Bind.bind (g x) h)) := by
+  simp [Bind.bind]
+  cases e <;> simp
+
 ----------
 -- MISC --
 ----------
-- 
cgit v1.2.3