Data.Linear.Bifunctor(source)

Definitions

bimap : (a -@ x) -@ ((b -@ y) -@ (LPair a b -@ LPair x y))

  A linear bimap on linear pairs.
  There is no general Bifunctor interface because it would not be implementable with
  The same type signature consistently, for example LEither does not consume both
  `f` and `g` linearly.

Totality: total
Visibility: public export

mapFst : (a -@ x) -@ (LPair a b -@ LPair x b)

Totality: total
Visibility: public export

mapSnd : (b -@ y) -@ (LPair a b -@ LPair a y)

Totality: total
Visibility: public export