git.iko.soy/Idris-dev
on master help sign in
Extract "swap" on Either to Prelude

This function was defined in multiple where-blocks in the Prelude and Base. It caused a scoping issue with one of them, and it is in general just cleaner to have it in one place.

commitc18f17b714ec7aeb0dc9bfbdfce63bc0439a8b31 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 20 Apr 2015, 12:18 (12 years ago) parent6f30060
3 files changed+7−8
compare with master
unifiedsplit
libs/base/Control/Arrow.idr+1−4 libs/base/Control/Isomorphism.idr+1−4 libs/prelude/Prelude/Either.idr+5
libs/base/Control/Arrow.idr+1−4
@@ -61,10 +61,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
6161 left : arr a b -> arr (Either a c) (Either b c)
6262
6363 right : arr a b -> arr (Either c a) (Either c b)
64− right f = arrow swap >>> left f >>> arrow swap where
65− swap : Either a b -> Either b a
66− swap (Left x) = Right x
67− swap (Right x) = Left x
64+ right f = arrow swap >>> left f >>> arrow swap
6865
6966 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
7067 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
4040||| Disjunction is commutative
4141eitherComm : Iso (Either a b) (Either b a)
4242eitherComm = 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
4744 swapSwap (Left x) = Refl
4845 swapSwap (Right x) = Refl
4946
libs/prelude/Prelude/Either.idr+5
@@ -66,6 +66,11 @@ fromEither : Either a a -> a
6666fromEither (Left l) = l
6767fromEither (Right r) = r
6868
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+
6974--------------------------------------------------------------------------------
7075-- Conversions
7176--------------------------------------------------------------------------------