Data.Either.Extra

Definitions

fromLeft : (b -> a) -> Either a b -> a

Totality: total
Visibility: public export

fromRight : (a -> b) -> Either a b -> b

Totality: total
Visibility: public export

mapFstExtensional : ((x : a) -> f x = g x) -> (v : Either a c) -> mapFst f v = mapFst g v

Totality: total
Visibility: export

mapSndExtensional : ((x : a) -> f x = g x) -> (v : Either w a) -> mapSnd f v = mapSnd g v

Totality: total
Visibility: export

mapFstFusion : (v : Either a e) -> mapFst g (mapFst f v) = mapFst (g . f) v

Totality: total
Visibility: export

mapSndFusion : (v : Either w a) -> mapSnd g (mapSnd f v) = mapSnd (g . f) v

Totality: total
Visibility: export