    {-# LANGUAGE CPP  #-}

    -- | More monoids.

    module Agda.Utils.Monoid where

    #if !(MIN_VERSION_base(4,11,0))
    import Data.Semigroup (Semigroup(..))
    #endif

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

    newtype MaxNat = MaxNat { MaxNat -> Int
    getMaxNat :: Int }
      deriving (Integer -> MaxNat
    MaxNat -> MaxNat
    MaxNat -> MaxNat -> MaxNat
    (MaxNat -> MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat)
    -> (Integer -> MaxNat)
    -> Num MaxNat
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    fromInteger :: Integer -> MaxNat
    $cfromInteger :: Integer -> MaxNat
    signum :: MaxNat -> MaxNat
    $csignum :: MaxNat -> MaxNat
    abs :: MaxNat -> MaxNat
    $cabs :: MaxNat -> MaxNat
    negate :: MaxNat -> MaxNat
    $cnegate :: MaxNat -> MaxNat
    * :: MaxNat -> MaxNat -> MaxNat
    $c* :: MaxNat -> MaxNat -> MaxNat
    - :: MaxNat -> MaxNat -> MaxNat
    $c- :: MaxNat -> MaxNat -> MaxNat
    + :: MaxNat -> MaxNat -> MaxNat
    $c+ :: MaxNat -> MaxNat -> MaxNat
    Num, MaxNat -> MaxNat -> Bool
    (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> Bool) -> Eq MaxNat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: MaxNat -> MaxNat -> Bool
    $c/= :: MaxNat -> MaxNat -> Bool
    == :: MaxNat -> MaxNat -> Bool
    $c== :: MaxNat -> MaxNat -> Bool
    Eq, Eq MaxNat
    Eq MaxNat
    -> (MaxNat -> MaxNat -> Ordering)
    -> (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat -> MaxNat)
    -> Ord MaxNat
    MaxNat -> MaxNat -> Bool
    MaxNat -> MaxNat -> Ordering
    MaxNat -> MaxNat -> MaxNat
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: MaxNat -> MaxNat -> MaxNat
    $cmin :: MaxNat -> MaxNat -> MaxNat
    max :: MaxNat -> MaxNat -> MaxNat
    $cmax :: MaxNat -> MaxNat -> MaxNat
    >= :: MaxNat -> MaxNat -> Bool
    $c>= :: MaxNat -> MaxNat -> Bool
    > :: MaxNat -> MaxNat -> Bool
    $c> :: MaxNat -> MaxNat -> Bool
    <= :: MaxNat -> MaxNat -> Bool
    $c<= :: MaxNat -> MaxNat -> Bool
    < :: MaxNat -> MaxNat -> Bool
    $c< :: MaxNat -> MaxNat -> Bool
    compare :: MaxNat -> MaxNat -> Ordering
    $ccompare :: MaxNat -> MaxNat -> Ordering
    Ord, Int -> MaxNat -> ShowS
    [MaxNat] -> ShowS
    MaxNat -> String
    (Int -> MaxNat -> ShowS)
    -> (MaxNat -> String) -> ([MaxNat] -> ShowS) -> Show MaxNat
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [MaxNat] -> ShowS
    $cshowList :: [MaxNat] -> ShowS
    show :: MaxNat -> String
    $cshow :: MaxNat -> String
    showsPrec :: Int -> MaxNat -> ShowS
    $cshowsPrec :: Int -> MaxNat -> ShowS
    Show, Int -> MaxNat
    MaxNat -> Int
    MaxNat -> [MaxNat]
    MaxNat -> MaxNat
    MaxNat -> MaxNat -> [MaxNat]
    MaxNat -> MaxNat -> MaxNat -> [MaxNat]
    (MaxNat -> MaxNat)
    -> (MaxNat -> MaxNat)
    -> (Int -> MaxNat)
    -> (MaxNat -> Int)
    -> (MaxNat -> [MaxNat])
    -> (MaxNat -> MaxNat -> [MaxNat])
    -> (MaxNat -> MaxNat -> [MaxNat])
    -> (MaxNat -> MaxNat -> MaxNat -> [MaxNat])
    -> Enum MaxNat
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat]
    $cenumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat]
    enumFromTo :: MaxNat -> MaxNat -> [MaxNat]
    $cenumFromTo :: MaxNat -> MaxNat -> [MaxNat]
    enumFromThen :: MaxNat -> MaxNat -> [MaxNat]
    $cenumFromThen :: MaxNat -> MaxNat -> [MaxNat]
    enumFrom :: MaxNat -> [MaxNat]
    $cenumFrom :: MaxNat -> [MaxNat]
    fromEnum :: MaxNat -> Int
    $cfromEnum :: MaxNat -> Int
    toEnum :: Int -> MaxNat
    $ctoEnum :: Int -> MaxNat
    pred :: MaxNat -> MaxNat
    $cpred :: MaxNat -> MaxNat
    succ :: MaxNat -> MaxNat
    $csucc :: MaxNat -> MaxNat
    Enum)

    instance Semigroup MaxNat where
      <> :: MaxNat -> MaxNat -> MaxNat
    (<>) = MaxNat -> MaxNat -> MaxNat
    forall a. Ord a => a -> a -> a
    max

    instance Monoid MaxNat where
      mempty :: MaxNat
    mempty     = MaxNat
    0
    #if !(MIN_VERSION_base(4,11,0))
      mappend    = (<>)
    #endif
      mconcat :: [MaxNat] -> MaxNat
    mconcat [] = MaxNat
    0
      mconcat [MaxNat]
    ms = [MaxNat] -> MaxNat
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [MaxNat]
    ms