    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | More monoids.

    module Agda.Utils.Monoid where

    -- | 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
    $c+ :: MaxNat -> MaxNat -> MaxNat
    + :: MaxNat -> MaxNat -> MaxNat
    $c- :: MaxNat -> MaxNat -> MaxNat
    - :: MaxNat -> MaxNat -> MaxNat
    $c* :: MaxNat -> MaxNat -> MaxNat
    * :: MaxNat -> MaxNat -> MaxNat
    $cnegate :: MaxNat -> MaxNat
    negate :: MaxNat -> MaxNat
    $cabs :: MaxNat -> MaxNat
    abs :: MaxNat -> MaxNat
    $csignum :: MaxNat -> MaxNat
    signum :: MaxNat -> MaxNat
    $cfromInteger :: Integer -> MaxNat
    fromInteger :: Integer -> MaxNat
    Num, MaxNat -> MaxNat -> Bool
    (MaxNat -> MaxNat -> Bool)
    -> (MaxNat -> MaxNat -> Bool) -> Eq MaxNat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: MaxNat -> MaxNat -> Bool
    == :: MaxNat -> MaxNat -> Bool
    $c/= :: MaxNat -> MaxNat -> Bool
    /= :: 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
    $ccompare :: MaxNat -> MaxNat -> Ordering
    compare :: MaxNat -> MaxNat -> Ordering
    $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
    >= :: MaxNat -> MaxNat -> Bool
    $cmax :: MaxNat -> MaxNat -> MaxNat
    max :: MaxNat -> MaxNat -> MaxNat
    $cmin :: MaxNat -> MaxNat -> MaxNat
    min :: MaxNat -> MaxNat -> MaxNat
    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
    $cshowsPrec :: Int -> MaxNat -> ShowS
    showsPrec :: Int -> MaxNat -> ShowS
    $cshow :: MaxNat -> String
    show :: MaxNat -> String
    $cshowList :: [MaxNat] -> ShowS
    showList :: [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
    $csucc :: MaxNat -> MaxNat
    succ :: MaxNat -> MaxNat
    $cpred :: MaxNat -> MaxNat
    pred :: MaxNat -> MaxNat
    $ctoEnum :: Int -> MaxNat
    toEnum :: Int -> MaxNat
    $cfromEnum :: MaxNat -> Int
    fromEnum :: MaxNat -> Int
    $cenumFrom :: MaxNat -> [MaxNat]
    enumFrom :: MaxNat -> [MaxNat]
    $cenumFromThen :: MaxNat -> MaxNat -> [MaxNat]
    enumFromThen :: MaxNat -> MaxNat -> [MaxNat]
    $cenumFromTo :: MaxNat -> MaxNat -> [MaxNat]
    enumFromTo :: MaxNat -> MaxNat -> [MaxNat]
    $cenumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat]
    enumFromThenTo :: MaxNat -> MaxNat -> 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
      mconcat :: [MaxNat] -> MaxNat
    mconcat [] = MaxNat
    0
      mconcat [MaxNat]
    ms = [MaxNat] -> MaxNat
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [MaxNat]
    ms