    {-# LANGUAGE GeneralizedNewtypeDeriving #-}

    -- | More monoids.

    module Agda.Utils.Monoid where

    import Data.Semigroup (Semigroup(..))
    import Data.Monoid (Monoid(..))

    -- | Maximum of on-negative (small) natural numbers.

    newtype MaxNat = MaxNat { getMaxNat :: Int }
      deriving (Num, Eq, Ord, Show, Enum)

    instance Semigroup MaxNat where
      (<>) = max

    instance Monoid MaxNat where
      mempty     = 0
      mappend    = (<>)
      mconcat [] = 0
      mconcat ms = maximum ms