c18f17b · Idris-dev · git.iko.soy

libs/base/Control/Arrow.idr+1−4

compare with master

unifiedsplit

@@ -61,10 +61,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where

61 left : arr a b -> arr (Either a c) (Either b c)

62

63 right : arr a b -> arr (Either c a) (Either c b)

64− right f = arrow swap >>> left f >>> arrow swap where

64+ right f = arrow swap >>> left f >>> arrow swap

65− swap : Either a b -> Either b a

66− swap (Left x) = Right x

67− swap (Right x) = Left x

68

65

69 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)

66 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)

70 f +++ g = left f >>> right g

67 f +++ g = left f >>> right g

libs/base/Control/Isomorphism.idr+1−4

@@ -40,10 +40,7 @@ isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

40||| Disjunction is commutative

41eitherComm : Iso (Either a b) (Either b a)

42eitherComm = MkIso swap swap swapSwap swapSwap

43− where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!

44− swap (Left x) = Right x

45− swap (Right x) = Left x

46− swapSwap : (e : Either a' b') -> swap (swap e) = e

43+ where swapSwap : (e : Either a' b') -> swap (swap e) = e

47 swapSwap (Left x) = Refl

44 swapSwap (Left x) = Refl

48 swapSwap (Right x) = Refl

45 swapSwap (Right x) = Refl

49

46

libs/prelude/Prelude/Either.idr+5

@@ -66,6 +66,11 @@ fromEither : Either a a -> a

66fromEither (Left l) = l

67fromEither (Right r) = r

68

69+||| Either is commutative

70+swap : Either a b -> Either b a

71+swap (Left x) = Right x

72+swap (Right x) = Left x

73+

69--------------------------------------------------------------------------------

74--------------------------------------------------------------------------------

70-- Conversions

75-- Conversions

71--------------------------------------------------------------------------------

76--------------------------------------------------------------------------------