From 33fe3f44dbe8a62068cf46d13f68f644c4036fb6 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sun, 20 Feb 2022 10:09:37 +0300 Subject: [PATCH] [ cleanup ] Clean up existing code in the `Arrow` module --- libs/contrib/Control/Arrow.idr | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr index 3500692be..13922d3b6 100644 --- a/libs/contrib/Control/Arrow.idr +++ b/libs/contrib/Control/Arrow.idr @@ -80,10 +80,6 @@ interface Arrow arr => ArrowChoice (0 arr : Type -> Type -> Type) where (\|/) : arr a b -> arr c b -> arr (Either a c) b f \|/ g = f +++ g >>> arrow fromEither - where - fromEither : Either b b -> b - fromEither (Left b) = b - fromEither (Right b) = b public export implementation Monad m => ArrowChoice (Kleislimorphism m) where @@ -102,10 +98,10 @@ implementation Monad m => ArrowApply (Kleislimorphism m) where public export data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where - MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a + MkArrowMonad : (runArrowMonad : arr Unit a) -> ArrowMonad arr a public export -runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a +runArrowMonad : ArrowMonad arr a -> arr Unit a runArrowMonad (MkArrowMonad a) = a public export