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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Monoid

Description

More monoids.

Synopsis

- newtype MaxNat = MaxNat {
  - getMaxNat :: Int
  }

# Documentation

newtype MaxNat Source #

Maximum of on-negative (small) natural numbers.

Constructors

MaxNat |

Fields

- getMaxNat :: Int

Instances

Enum MaxNat Source # |

Instance details

Defined in Agda.Utils.Monoid

Methods

succ :: MaxNat -> MaxNat Source #

pred :: MaxNat -> MaxNat Source #

toEnum :: Int -> MaxNat Source #

fromEnum :: MaxNat -> Int Source #

enumFrom :: MaxNat -> [MaxNat] Source #

enumFromThen :: MaxNat -> MaxNat -> [MaxNat] Source #

enumFromTo :: MaxNat -> MaxNat -> [MaxNat] Source #

enumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat] Source #

Eq MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods (==) :: MaxNat -> MaxNat -> Bool Source # (/=) :: MaxNat -> MaxNat -> Bool Source #
Num MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods (+) :: MaxNat -> MaxNat -> MaxNat Source # (-) :: MaxNat -> MaxNat -> MaxNat Source # (*) :: MaxNat -> MaxNat -> MaxNat Source # negate :: MaxNat -> MaxNat Source # abs :: MaxNat -> MaxNat Source # signum :: MaxNat -> MaxNat Source # fromInteger :: Integer -> MaxNat Source #
Ord MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods compare :: MaxNat -> MaxNat -> Ordering Source # (<) :: MaxNat -> MaxNat -> Bool Source # (<=) :: MaxNat -> MaxNat -> Bool Source # (>) :: MaxNat -> MaxNat -> Bool Source # (>=) :: MaxNat -> MaxNat -> Bool Source # max :: MaxNat -> MaxNat -> MaxNat Source # min :: MaxNat -> MaxNat -> MaxNat Source #
Show MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods showsPrec :: Int -> MaxNat -> ShowS Source # show :: MaxNat -> String Source # showList :: [MaxNat] -> ShowS Source #
Semigroup MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods (<>) :: MaxNat -> MaxNat -> MaxNat Source # sconcat :: NonEmpty MaxNat -> MaxNat Source # stimes :: Integral b => b -> MaxNat -> MaxNat Source #
Monoid MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods mempty :: MaxNat Source # mappend :: MaxNat -> MaxNat -> MaxNat Source # mconcat :: [MaxNat] -> MaxNat Source #