Data.Type.Natural

Re-exported modules.

Natural Numbers

data Nat

data SSym0 l

type SSym1 t

type ZSym0

type SNat z

data family Sing a

Smart constructors

Arithmetic functions and their singletons.

type family Min a a :: Nat

type family Max a a :: Nat

data MinSym0 l

data MinSym1 l l

type MinSym2 t t

data MaxSym0 l

data MaxSym1 l l

type MaxSym2 t t

type n :+: m

type family a :+ a :: Nat

data (:+$) l

data l :+$$ l

type t :+$$$ t

type family a :* a :: Nat

type n :*: m

data (:*$) l

data l :*$$ l

type t :*$$$ t

type n :-: m

type family a :- a :: Nat

type n :**: m

type family a :** a :: Nat

data (:-$) l

data l :-$$ l

type t :-$$$ t

Type-level predicate & judgements

data Leq n m

class n :<= m

type family a :<<= a :: Bool

data (:<<=$) l

data l :<<=$$ l

type t :<<=$$$ t

type LeqInstance n m

type LeqTrueInstance a b

Conversion functions

Quasi quotes for natural numbers

Properties of natural numbers

plusAssociative

multAssociative

plusCommutative

Properties of ordering `Leq`

leqAnitsymmetric

Useful type synonyms and constructors

type Zero

type One

type Two

type Three

type Four

type Five

type Six

type Seven

type Eight

type Nine

type Ten

type ElevenSym0

type TwelveSym0

type ThirteenSym0

type FourteenSym0

type FifteenSym0

type SixteenSym0

type SeventeenSym0

type EighteenSym0

type NineteenSym0

type TwentySym0

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