Data.Constraint.Nat
type family Min :: Nat -> Nat -> Nat where ...
type family Max :: Nat -> Nat -> Nat where ...
type family Lcm :: Nat -> Nat -> Nat where ...
type family Gcd :: Nat -> Nat -> Nat where ...
type Divides n m
type family Div :: Nat -> Nat -> Nat where ...
type family Mod :: Nat -> Nat -> Nat where ...
plusNat
timesNat
powNat
minNat
maxNat
gcdNat
lcmNat
divNat
modNat
plusZero
timesZero
timesOne
powZero
powOne
maxZero
minZero
gcdZero
gcdOne
lcmZero
lcmOne
plusAssociates
timesAssociates
minAssociates
maxAssociates
gcdAssociates
lcmAssociates
plusCommutes
timesCommutes
minCommutes
maxCommutes
gcdCommutes
lcmCommutes
plusDistributesOverTimes
timesDistributesOverPow
timesDistributesOverGcd
timesDistributesOverLcm
minDistributesOverPlus
minDistributesOverTimes
minDistributesOverPow1
minDistributesOverPow2
minDistributesOverMax
maxDistributesOverPlus
maxDistributesOverTimes
maxDistributesOverPow1
maxDistributesOverPow2
maxDistributesOverMin
gcdDistributesOverLcm
lcmDistributesOverGcd
minIsIdempotent
maxIsIdempotent
lcmIsIdempotent
gcdIsIdempotent
plusIsCancellative
timesIsCancellative
dividesPlus
dividesTimes
dividesMin
dividesMax
dividesPow
dividesGcd
dividesLcm
plusMonotone1
plusMonotone2
timesMonotone1
timesMonotone2
powMonotone1
powMonotone2
minMonotone1
minMonotone2
maxMonotone1
maxMonotone2
divMonotone1
divMonotone2
euclideanNat
plusMod
timesMod
modBound
dividesDef
timesDiv
eqLe
leEq
leId
leTrans
leZero
zeroLe