Adjust state monad utils

MetaCoq · Apr 24, 2023 · d538d2f · d538d2f
1 parent b33c544
commit d538d2f
Showing 1 changed file with 10 additions and 6 deletions.
diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v
@@ -77,12 +77,16 @@ Definition StateT_Monad {S T} {TM : Monad T} : Monad (StateT S T) :=
   |}.
 #[export] Hint Extern 1 (Monad (StateT ?S ?T)) => simple apply (@StateT_Monad S T) : typeclass_instances.
 
-Definition get_state {S T} {TM : Monad T} : StateT S T S
-  := fun s => ret (s, s).
-Definition update_state {S T} {TM : Monad T} (f : S -> S) : StateT S T unit
-  := fun s => ret (tt, f s).
-Definition set_state {S T} {TM : Monad T} (s : S) : StateT S T unit
-  := update_state (fun _ => s).
+Module State.
+  Definition get {S T} {TM : Monad T} : StateT S T S
+    := fun s => ret (s, s).
+  Definition update {S T} {TM : Monad T} (f : S -> S) : StateT S T unit
+    := fun s => ret (tt, f s).
+  Definition set {S T} {TM : Monad T} (s : S) : StateT S T unit
+    := update (fun _ => s).
+  Definition lift {S T} {TM : Monad T} {A} (m : T A) : StateT S T A
+    := fun s => v <- m;; ret (v, s).
+End State.
 
 Section MapOpt.
   Context {A} {B} (f : A -> option B).