From 12612bb494457096c1a720c0c1ffb4357cf39e62 Mon Sep 17 00:00:00 2001
From: br <Burkhardt.Renz@mni.thm.de>
Date: Wed, 4 Feb 2026 08:20:10 +0100
Subject: [PATCH] TimeM is a LawfulMonad

---
 Cslib/Algorithms/Lean/TimeM.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean
index ff7f0f738..3d1ff5c9a 100644
--- a/Cslib/Algorithms/Lean/TimeM.lean
+++ b/Cslib/Algorithms/Lean/TimeM.lean
@@ -63,6 +63,20 @@ instance : Monad TimeM where
   pure := pure
   bind := bind
 
+instance : LawfulMonad TimeM := .mk'
+  (id_map := fun x => by rfl)
+  (pure_bind := by
+    intros
+    simp only [Bind.bind, Pure.pure]
+    rw [bind, pure]
+    simp)
+  (bind_assoc := by
+    intros
+    simp only [Bind.bind]
+    unfold bind
+    simp only [mk.injEq, true_and]
+    ac_rfl)
+
 /-- Creates a `TimeM` computation with a specified value and time cost.
 The time cost defaults to 1 if not provided. -/
 @[simp, grind =] def tick {α : Type*} (a : α) (c : ℕ := 1) : TimeM α := ⟨a, c⟩