feat: add LawfulMonad instance for EStateM (#416)

Co-authored-by: François G. Dorais <fgdorais@gmail.com>
leanprover-community · Dec 5, 2023 · baf6def · baf6def
1 parent 1f24793
commit baf6def
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/Std/Classes/LawfulMonad.lean b/Std/Classes/LawfulMonad.lean
@@ -52,6 +52,20 @@ instance : LawfulMonad Option := LawfulMonad.mk'
 instance : LawfulApplicative Option := inferInstance
 instance : LawfulFunctor Option := inferInstance
 
+instance : LawfulMonad (EStateM ε σ) := .mk'
+  (id_map := fun x => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (map_const := fun _ _ => rfl)
+
 /-!
 ## SatisfiesM