idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] Clean up existing code in the Arrow module

Browse Source
This commit is contained in:
Denis Buzdalov 2022-02-20 10:09:37 +03:00 committed by G. Allais
parent c8f625cad9
commit 33fe3f44db
1 changed files with 2 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/contrib/Control/Arrow.idr
View File

@ -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