Re-exported modules.

Natural Numbers

data Nat

data SSym0 l

type SSym1 t

type ZSym0

type SNat

data family Sing k (a :: k) :: *

Arithmetic functions and their singletons.

min

type family Min a0 (arg0 :: a0) (arg1 :: a0) :: a0

sMin

max

type family Max a0 (arg0 :: a0) (arg1 :: a0) :: a0

sMax

data MinSym0 a1627675388 l0

data MinSym1 a1627675388 l0 l1

type MinSym2 a1627675388 t0 t1

data MaxSym0 a1627675388 l0

data MaxSym1 a1627675388 l0 l1

type MaxSym2 a1627675388 t0 t1

type n :+: m

type family (a0 :+ (arg0 :: a0)) (arg1 :: a0) :: a0

data a1627810386 :+$ l0

data (a1627810386 :+$$ l0) l1

type (a1627810386 :+$$$ t0) t1

(%+)

(%:+)

type family (a0 :* (arg0 :: a0)) (arg1 :: a0) :: a0

type n :*: m

data a1627810386 :*$ l0

data (a1627810386 :*$$ l0) l1

type (a1627810386 :*$$$ t0) t1

(%:*)

(%*)

type n :-: m

type family (a0 :- (arg0 :: a0)) (arg1 :: a0) :: a0

type n :**: m

type family (a :: Nat) :** (a :: Nat) :: Nat where ...

(%:**)

(%**)

data a1627810386 :-$ l0

data (a1627810386 :-$$ l0) l1

type (a1627810386 :-$$$ t0) t1

(%:-)

(%-)

Type-level predicate & judgements

data Leq n m

class n :<= m

type family (a :: Nat) :<<= (a :: Nat) :: Bool where ...

data (:<<=$) l

data l :<<=$$ l

type t :<<=$$$ t

type LeqInstance n m

type LeqTrueInstance a b

propToBoolLeq

Conversion functions

natToInt

intToNat

sNatToInt

Quasi quotes for natural numbers

nat

snat

Properties of natural numbers

Properties of ordering `Leq`

Useful type synonyms and constructors

type family Zero :: Nat where ...

type family One :: Nat where ...

type family Two :: Nat where ...

type family Three :: Nat where ...

type family Four :: Nat where ...

type family Five :: Nat where ...

type family Six :: Nat where ...

type family Seven :: Nat where ...

type family Eight :: Nat where ...

type family Nine :: Nat where ...

type family Ten :: Nat where ...

type family Eleven :: Nat where ...

type family Twelve :: Nat where ...

type family Thirteen :: Nat where ...

type family Fourteen :: Nat where ...

type family Fifteen :: Nat where ...

type family Sixteen :: Nat where ...

type family Seventeen :: Nat where ...

type family Eighteen :: Nat where ...

type family Nineteen :: Nat where ...

type family Twenty :: Nat where ...

type ZeroSym0

type OneSym0

type TwoSym0

type ThreeSym0

type FourSym0

type FiveSym0

type SixSym0

type SevenSym0

type EightSym0

type NineSym0

type TenSym0

type ElevenSym0

type TwelveSym0

type ThirteenSym0

type FourteenSym0

type FifteenSym0

type SixteenSym0

type SeventeenSym0

type EighteenSym0

type NineteenSym0

type TwentySym0

type family N0 :: Nat where ...

type family N1 :: Nat where ...

type family N2 :: Nat where ...

type family N3 :: Nat where ...

type family N4 :: Nat where ...

type family N5 :: Nat where ...

type family N6 :: Nat where ...

type family N7 :: Nat where ...

type family N8 :: Nat where ...

type family N9 :: Nat where ...

type family N10 :: Nat where ...

type family N11 :: Nat where ...

type family N12 :: Nat where ...

type family N13 :: Nat where ...

type family N14 :: Nat where ...

type family N15 :: Nat where ...

type family N16 :: Nat where ...

type family N17 :: Nat where ...

type family N18 :: Nat where ...

type family N19 :: Nat where ...

type family N20 :: Nat where ...

type N0Sym0

type N1Sym0

type N2Sym0

type N3Sym0

type N4Sym0

type N5Sym0

type N6Sym0

type N7Sym0

type N8Sym0

type N9Sym0

type N10Sym0

type N11Sym0

type N12Sym0

type N13Sym0

type N14Sym0

type N15Sym0

type N16Sym0

type N17Sym0

type N18Sym0

type N19Sym0

type N20Sym0