Type.Family.Nat

data N

fromInt

type family IsZero (x :: N) :: Bool where ...

zeroCong

zNotS

type family NatEq (x :: N) (y :: N) :: Bool where ...

type family Iota (x :: N) = (xs :: [N]) | xs -> x where ...

iotaCong

type family Pred (x :: N) :: N where ...

type Pos n

predCong

type family (x :: N) + (y :: N) :: N where ...

data AddW f

addCong

type family (x :: N) * (y :: N) :: N where ...

data MulW f

mulCong

type family (x :: N) ^ (y :: N) :: N where ...

expCong

type family Len (as :: [k]) :: N where ...

lenCong

type family Ix (x :: N) (as :: [k]) :: k where ...

ixCong

type family (x :: N) < (y :: N) :: Bool where ...

type x <= y

type family (x :: N) > (y :: N) :: Bool where ...

type x >= y

type N0

type N1

type N2

type N3

type N4

type N5

type N6

type N7

type N8

type N9

type N10