From b0798adc8d7046f85cf0a2ef84ace63a4f84441f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 10 Jul 2024 16:43:50 +0900 Subject: [PATCH] minor edits --- impredicative_set/imonad_lib.v | 2 +- monad_lib.v | 2 +- monad_transformer.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/impredicative_set/imonad_lib.v b/impredicative_set/imonad_lib.v index 1899d6d9..b0a781cc 100644 --- a/impredicative_set/imonad_lib.v +++ b/impredicative_set/imonad_lib.v @@ -646,7 +646,7 @@ Qed. Definition commute {M : monad} A B (m : M A) (n : M B) C (f : A -> B -> M C) : Prop := m >>= (fun x => n >>= (fun y => f x y)) = - n >>= (fun y => m >>= (fun x => f x y)) :> M _. + n >>= (fun y => m >>= (fun x => f x y)). Definition preserves {M : monad} (A B : UU0) (f : A -> M A) (g : A -> B) := forall x, (f x >>= fun y => Ret (y, g y)) = (f x >>= fun y => Ret (y, g x)). diff --git a/monad_lib.v b/monad_lib.v index 535e8fe6..15cebda1 100644 --- a/monad_lib.v +++ b/monad_lib.v @@ -648,7 +648,7 @@ Qed. Definition commute {M : monad} A B (m : M A) (n : M B) C (f : A -> B -> M C) : Prop := m >>= (fun x => n >>= (fun y => f x y)) = - n >>= (fun y => m >>= (fun x => f x y)) :> M _. + n >>= (fun y => m >>= (fun x => f x y)). Definition preserves {M : monad} (A B : UU0) (f : A -> M A) (g : A -> B) := forall x, (f x >>= fun y => Ret (y, g y)) = (f x >>= fun y => Ret (y, g x)). diff --git a/monad_transformer.v b/monad_transformer.v index bbd0cd94..f6f916c9 100644 --- a/monad_transformer.v +++ b/monad_transformer.v @@ -152,7 +152,7 @@ Lemma MS_bindE [S : UU0] [M : monad] [A B : UU0] (m : MS S M A) (f : A -> MS S M (m >>= f) s = m s >>= uncurry f. Proof. by []. Qed. -Definition stateT (S : UU0) : monad -> monad := MS S. +Definition stateT : UU0 -> monad -> monad := MS. HB.instance Definition _ (S : UU0) := isMonadT.Build (stateT S) (@liftS S).