
  0 | module Data.Functor.Const
  1 | 
  2 | public export
  3 | record Const (a : Type) (b : Type) where
  4 |   constructor MkConst
  5 |   getConst : a
  6 | 
  7 | public export
  8 | Eq a => Eq (Const a b) where
  9 |   (==) = (==) `on` getConst
 10 | 
 11 | public export
 12 | Ord a => Ord (Const a b) where
 13 |   compare = compare `on` getConst
 14 | 
 15 | public export
 16 | Show a => Show (Const a b) where
 17 |   showPrec p = showCon p "MkConst" . showArg . getConst
 18 | 
 19 | public export
 20 | Functor (Const a) where
 21 |   map _ (MkConst a)= MkConst a
 22 | 
 23 | public export
 24 | Monoid a => Applicative (Const a) where
 25 |   pure _ = MkConst neutral
 26 |   MkConst f <*> MkConst a = MkConst $ f <+> a
 27 | 
 28 | public export
 29 | Foldable (Const a) where
 30 |   foldr _ acc _ = acc
 31 |   foldl _ acc _ = acc
 32 |   null        _ = True
 33 | 
 34 | public export
 35 | Traversable (Const a) where
 36 |   traverse _ (MkConst v) = pure (MkConst v)
 37 | 
 38 | public export
 39 | Bifunctor Const where
 40 |   bimap f _ (MkConst a) = MkConst (f a)
 41 | 
 42 | public export
 43 | Bifoldable Const where
 44 |   bifoldl f _ acc (MkConst a) = f acc a
 45 |   bifoldr f _ acc (MkConst a) = f a acc
 46 |   binull _ = False
 47 | 
 48 | public export
 49 | Bitraversable Const where
 50 |   bitraverse f _ (MkConst a) = MkConst <$> f a
 51 |