From d538d2f6ddb378945709b9589b38b69420cff78d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 20 Apr 2023 14:04:54 -0700 Subject: [PATCH] Adjust state monad utils --- utils/theories/monad_utils.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v index c33f7f219..0944c1a54 100644 --- 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).