Data.Type.Natural

Re-exported modules.

Natural Numbers

data Nat

type SNat a

data family Sing a

Smart constructors

sZ

sS

Arithmetic functions and their singletons.

min

type family Min a a :: Nat

sMin

max

type family Max a a :: Nat

sMax

type n :+: m

type family a :+ a :: Nat

(%+)

(%:+)

type n :*: m

type family a :* a :: Nat

(%:*)

(%*)

type n :-: m

type family a :- a :: Nat

(%:-)

(%-)

Type-level predicate & judgements

data Leq n m

class n :<= m

type family a :<<= a :: Bool

(%:<<=)

data LeqInstance n m

leqRefl

leqSucc

boolToPropLeq

boolToClassLeq

propToClassLeq

data LeqTrueInstance a b

propToBoolLeq

Conversion functions

natToInt

intToNat

sNatToInt

Quasi quotes for natural numbers

nat

snat

Properties of natural numbers

succCongEq

plusCongR

plusCongL

succPlusL

succPlusR

plusZR

plusZL

eqPreservesS

plusAssociative

multAssociative

multComm

multZL

multZR

multOneL

multOneR

plusMultDistr

multPlusDistr

multCongL

multCongR

sAndPlusOne

plusCommutative

minusCongEq

minusNilpotent

eqSuccMinus

plusMinusEqL

plusMinusEqR

plusLeqL

plusLeqR

zAbsorbsMinR

zAbsorbsMinL

minLeqL

minLeqR

plusSR

leqRhs

leqLhs

leqTrans

minComm

leqAnitsymmetric

maxZL

maxComm

maxZR

maxLeqL

maxLeqR

plusMonotone

Useful type synonyms and constructors

zero

one

two

three

four

five

six

seven

eight

nine

ten

eleven

twelve

thirteen

fourteen

fifteen

sixteen

seventeen

eighteen

nineteen

twenty

type Zero

type One

type Two

type Three

type Four

type Five

type Six

type Seven

type Eight

type Nine

type Ten

type Eleven

type Twelve

type Thirteen

type Fourteen

type Fifteen

type Sixteen

type Seventeen

type Eighteen

type Nineteen

type Twenty

sZero

sOne

sTwo

sThree

sFour

sFive

sSix

sSeven

sEight

sNine

sTen

sEleven

sTwelve

sThirteen

sFourteen

sFifteen

sSixteen

sSeventeen

sEighteen

sNineteen

sTwenty

n0

n1

n2

n3

n4

n5

n6

n7

n8

n9

n10

n11

n12

n13

n14

n15

n16

n17

n18

n19

n20

type N0

type N1

type N2

type N3

type N4

type N5

type N6

type N7

type N8

type N9

type N10

type N11

type N12

type N13

type N14

type N15

type N16

type N17

type N18

type N19

type N20

sN0

sN1

sN2

sN3

sN4

sN5

sN6

sN7

sN8

sN9

sN10

sN11

sN12

sN13

sN14

sN15

sN16

sN17

sN18

sN19

sN20