module Integer.StrictlyIncrease where

import Integer.Integer (Integer)
import Integer.Integer qualified as Integer
import Integer.Natural (Natural)
import Integer.Natural qualified as Natural
import Integer.Positive (Positive)
import Integer.Signed (Signed)
import Integer.Signed qualified as Signed
import Prelude qualified as Num (Num (..))

-- | Class of numbers that are closed under addition with 'Positive'
class StrictlyIncrease a where
  -- | Addition
  strictlyIncrease :: Positive -> a -> a

instance StrictlyIncrease Integer where
  strictlyIncrease :: Positive -> Integer -> Integer
strictlyIncrease = Positive -> Integer -> Integer
Integer.strictlyIncrease

instance StrictlyIncrease Signed where
  strictlyIncrease :: Positive -> Signed -> Signed
strictlyIncrease = Positive -> Signed -> Signed
Signed.strictlyIncrease

instance StrictlyIncrease Natural where
  strictlyIncrease :: Positive -> Natural -> Natural
strictlyIncrease = Positive -> Natural -> Natural
Natural.strictlyIncrease

instance StrictlyIncrease Positive where
  strictlyIncrease :: Positive -> Positive -> Positive
strictlyIncrease = forall a. Num a => a -> a -> a
(Num.+)