Idris2Doc : Data.Either.Extra

Data.Either.Extra

Definitions

fromLeft : (b->a) ->Eitherab->a
Totality: total
Visibility: public export
fromRight : (a->b) ->Eitherab->b
Totality: total
Visibility: public export
mapFstExtensional : ((x : a) ->fx=gx) -> (v : Eitherac) ->mapFstfv=mapFstgv
Totality: total
Visibility: export
mapSndExtensional : ((x : a) ->fx=gx) -> (v : Eitherwa) ->mapSndfv=mapSndgv
Totality: total
Visibility: export
mapFstFusion : (v : Eitherae) ->mapFstg (mapFstfv) =mapFst (g.f) v
Totality: total
Visibility: export
mapSndFusion : (v : Eitherwa) ->mapSndg (mapSndfv) =mapSnd (g.f) v
Totality: total
Visibility: export