Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe Haskell	None
Language	Haskell2010

Agda.Utils.Monoid

Description

More monoids.

Synopsis

Documentation

newtype MaxNat Source #

Maximum of on-negative (small) natural numbers.

Constructors

MaxNat
Fields getMaxNat :: Int

Instances

Enum MaxNat Source #
Methods succ :: MaxNat -> MaxNat # pred :: MaxNat -> MaxNat # toEnum :: Int -> MaxNat # fromEnum :: MaxNat -> Int # enumFrom :: MaxNat -> [MaxNat] # enumFromThen :: MaxNat -> MaxNat -> [MaxNat] # enumFromTo :: MaxNat -> MaxNat -> [MaxNat] # enumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat] #
Eq MaxNat Source #
Methods (==) :: MaxNat -> MaxNat -> Bool # (/=) :: MaxNat -> MaxNat -> Bool #
Num MaxNat Source #
Methods (+) :: MaxNat -> MaxNat -> MaxNat # (-) :: MaxNat -> MaxNat -> MaxNat # (*) :: MaxNat -> MaxNat -> MaxNat # negate :: MaxNat -> MaxNat # abs :: MaxNat -> MaxNat # signum :: MaxNat -> MaxNat # fromInteger :: Integer -> MaxNat #
Ord MaxNat Source #
Methods compare :: MaxNat -> MaxNat -> Ordering # (<) :: MaxNat -> MaxNat -> Bool # (<=) :: MaxNat -> MaxNat -> Bool # (>) :: MaxNat -> MaxNat -> Bool # (>=) :: MaxNat -> MaxNat -> Bool # max :: MaxNat -> MaxNat -> MaxNat # min :: MaxNat -> MaxNat -> MaxNat #
Show MaxNat Source #
Methods showsPrec :: Int -> MaxNat -> ShowS # show :: MaxNat -> String # showList :: [MaxNat] -> ShowS #
Semigroup MaxNat Source #
Methods (<>) :: MaxNat -> MaxNat -> MaxNat # sconcat :: NonEmpty MaxNat -> MaxNat # stimes :: Integral b => b -> MaxNat -> MaxNat #
Monoid MaxNat Source #
Methods mempty :: MaxNat # mappend :: MaxNat -> MaxNat -> MaxNat # mconcat :: [MaxNat] -> MaxNat #