Data.Nat

Documentation

data Nat

Constructors

Z

S Nat

Instances

Eq Nat

Ord Nat

Show Nat

SingI Nat Z

POrd Nat (KProxy Nat)

SEq Nat (KProxy Nat)

PEq Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

SingI Nat n0 => SingI Nat (S n)

SingKind Nat (KProxy Nat)

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:*$$)

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:*$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:+$)

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

data Sing Nat where

• SZ :: (~) Nat z Z => Sing Nat z
• SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z

type Compare Nat Z Z = EQ

type (:==) Nat a0 b0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type Compare Nat Z (S rhs0) = LT

type Apply Nat Nat ((:*$$) l1) l0

type Apply Nat Nat ((:+$$) l1) l0

type DemoteRep Nat (KProxy Nat) = Nat

type Compare Nat (S lhs0) Z = GT

type Compare Nat (S lhs0) (S rhs0) = ThenCmp EQ (Compare Nat lhs0 rhs0)

type Apply (TyFun Nat Nat -> *) Nat (:*$) l0 = (:*$$) l0

type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0

(+) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

type SNat z = Sing z

type family a :* a :: Nat

Equations

Z :* b = ZSym0

(S a) :* b = Apply (Apply (:+$) b) (Apply (Apply (:*$) a) b)

data (:*$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:*$)

type Apply (TyFun Nat Nat -> *) Nat (:*$) l0 = (:*$$) l0

data l :*$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:*$$)

type Apply Nat Nat ((:*$$) l1) l0

type family a :+ a :: Nat

Equations

Z :+ b = b

(S a) :+ b = Apply SSym0 (Apply (Apply (:+$) a) b)

data (:+$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:+$)

type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0

data l :+$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$)

type Apply Nat Nat ((:+$$) l1) l0

data SSym0 l

Constructors

forall arg . (KindOf (Apply SSym0 arg) ~ KindOf (SSym1 arg)) => SSym0KindInference

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t

type ZSym0 = Z

(%:+) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t)

(%:*) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:*$) t) t)

type family Lit n

Equations

Lit 0 = Z

Lit n = S (Lit (n - 1))

type SLit n = Sing (Lit n)