From a2670f4d097075c23b9affceb8ed8498b73c4b8c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 19 Jun 2023 18:52:29 +0200
Subject: Cleanup Diverge.lean

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

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

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index d6cc0bad..1185a07d 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -94,6 +94,10 @@ instance : Bind Result where
 instance : Pure Result where
   pure := fun x => ret x
 
+@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
+@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
+
 /- CUSTOM-DSL SUPPORT -/
 
 -- Let-binding the Result of a monadic operation is oftentimes not sufficient,
@@ -124,6 +128,15 @@ macro "let" e:term " <-- " f:term : doElem =>
   let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩
   .ret r
 
+@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
+  (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
+  (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_div (f : α → Result β) :
+  (do let y ← div; f y) = div := by simp [Bind.bind, bind]
+
 ----------------------
 -- MACHINE INTEGERS --
 ----------------------
-- 
cgit v1.2.3