Data.Type.Natural

Type level peano natural number, some arithmetic functions and their singletons.

Re-exported modules.

module Data.Singletons

Natural Numbers

Peano natural numbers. It will be promoted to the type-level natural number.

data Nat

Constructors

Z

S Nat

Instances

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Num Nat

Methods

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

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

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

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

SingKind Nat

Associated Types

type DemoteRep Nat :: *

Methods

fromSing :: Sing Nat a -> DemoteRep Nat

toSing :: DemoteRep Nat -> SomeSing Nat

SNum Nat

Methods

(%:+) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t0) t1)

(%:-) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t0) t1)

(%:*) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:*$) Nat) t0) t1)

sNegate :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t0)

sAbs :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t0)

sSignum :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t0)

sFromInteger :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t0)

SOrd Nat

Methods

sCompare :: Sing Nat t0 -> Sing Nat t1 -> Sing Ordering (Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (CompareSym0 Nat) t0) t1)

(%:<) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<$) Nat) t0) t1)

(%:<=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<=$) Nat) t0) t1)

(%:>) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>$) Nat) t0) t1)

(%:>=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>=$) Nat) t0) t1)

sMax :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MaxSym0 Nat) t0) t1)

sMin :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MinSym0 Nat) t0) t1)

SEq Nat

Methods

(%:==) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :== a) b)

(%:/=) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :/= a) b)

SDecide Nat

Methods

(%~) :: Sing Nat a -> Sing Nat b -> Decision ((Nat :~: a) b)

SingI Nat Z

Methods

sing :: Sing Z a

SingI Nat n0 => SingI Nat (S n0)

Methods

sing :: Sing (S n0) a

PNum Nat (Proxy * Nat)

Associated Types

type ((Proxy * Nat) :+ (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type ((Proxy * Nat) :- (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type ((Proxy * Nat) :* (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type Negate (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type Abs (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type Signum (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type FromInteger (Proxy * Nat) (arg0 :: Nat) :: a0

POrd Nat (Proxy * Nat)

Associated Types

type Compare (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: Ordering

type ((Proxy * Nat) :< (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :<= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :> (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :>= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type Max (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0

type Min (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0

PEq Nat (Proxy * Nat)

Associated Types

type ((Proxy * Nat) :== (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :/= (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool

SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$)

Methods

suppressUnusedWarnings :: Proxy (:<<=$$) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> Type) -> *) (:<<=$)

Methods

suppressUnusedWarnings :: Proxy (:<<=$) t -> ()

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type DemoteRep Nat

type DemoteRep Nat = Nat

data Sing Nat

data Sing Nat where

• SZ :: Sing Nat z
• SS :: Sing Nat z

type FromInteger Nat a0

type FromInteger Nat a0

type Signum Nat a0

type Signum Nat a0

type Abs Nat a0

type Abs Nat a0

type Negate Nat arg0

type Negate Nat arg0 = Apply Nat Nat (Negate_1627810462Sym0 Nat) arg0

type (:*) Nat a0 a1

type (:*) Nat a0 a1

type (:-) Nat a0 a1

type (:-) Nat a0 a1

type (:+) Nat a0 a1

type (:+) Nat a0 a1

type Min Nat a0 a1

type Min Nat a0 a1

type Max Nat a0 a1

type Max Nat a0 a1

type (:>=) Nat arg0 arg1

type (:>=) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_1627676309Sym0 Nat) arg0) arg1

type (:>) Nat arg0 arg1

type (:>) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_1627676276Sym0 Nat) arg0) arg1

type (:<=) Nat a0 a1

type (:<=) Nat a0 a1

type (:<) Nat arg0 arg1

type (:<) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_1627676210Sym0 Nat) arg0) arg1

type Compare Nat arg0 arg1

type Compare Nat arg0 arg1 = Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (Compare_1627676177Sym0 Nat) arg0) arg1

type (:/=) Nat x y

type (:/=) Nat x y = Not ((:==) Nat x y)

type (:==) Nat a0 b0

type (:==) Nat a0 b0

type Apply Nat Nat SSym0 l0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type Apply Nat Bool ((:<<=$$) l1) l0

type Apply Nat Bool ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0

type MonomorphicRep Nat (Sing Nat)

type MonomorphicRep Nat (Sing Nat) = Int

type Apply Nat (TyFun Nat Bool -> Type) (:<<=$) l0

type Apply Nat (TyFun Nat Bool -> Type) (:<<=$) l0 = (:<<=$$) l0

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply Nat Nat SSym0 l0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t

type ZSym0 = Z

Singleton type for Nat.

type SNat = (Sing :: Nat -> Type)

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

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Nat

data Sing Nat where

• SZ :: Sing Nat z
• SS :: Sing Nat z

type MonomorphicRep Nat (Sing Nat)

type MonomorphicRep Nat (Sing Nat) = Int

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

Arithmetic functions and their singletons.

min :: Ord a => a -> a -> a

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

Instances

type Min Bool arg0 arg1

type Min Bool arg0 arg1 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Min_1627676375Sym0 Bool) arg0) arg1

type Min Ordering arg0 arg1

type Min Ordering arg0 arg1 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Min_1627676375Sym0 Ordering) arg0) arg1

type Min Nat arg0 arg1

type Min Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Min_1627676375Sym0 Nat) arg0) arg1

type Min Symbol arg0 arg1

type Min Symbol arg0 arg1 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Min_1627676375Sym0 Symbol) arg0) arg1

type Min () arg0 arg1

type Min () arg0 arg1 = Apply () () (Apply () (TyFun () () -> Type) (Min_1627676375Sym0 ()) arg0) arg1

type Min Nat a0 a1

type Min Nat a0 a1

type Min [a0] arg0 arg1

type Min [a0] arg0 arg1 = Apply [a0] [a0] (Apply [a0] (TyFun [a0] [a0] -> Type) (Min_1627676375Sym0 [a0]) arg0) arg1

type Min (Maybe a0) arg0 arg1

type Min (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (Maybe a0) (TyFun (Maybe a0) (Maybe a0) -> Type) (Min_1627676375Sym0 (Maybe a0)) arg0) arg1

type Min (NonEmpty a0) arg0 arg1

type Min (NonEmpty a0) arg0 arg1 = Apply (NonEmpty a0) (NonEmpty a0) (Apply (NonEmpty a0) (TyFun (NonEmpty a0) (NonEmpty a0) -> Type) (Min_1627676375Sym0 (NonEmpty a0)) arg0) arg1

type Min (Either a0 b0) arg0 arg1

type Min (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (Either a0 b0) (TyFun (Either a0 b0) (Either a0 b0) -> Type) (Min_1627676375Sym0 (Either a0 b0)) arg0) arg1

type Min (a0, b0) arg0 arg1

type Min (a0, b0) arg0 arg1 = Apply (a0, b0) (a0, b0) (Apply (a0, b0) (TyFun (a0, b0) (a0, b0) -> Type) (Min_1627676375Sym0 (a0, b0)) arg0) arg1

type Min (a0, b0, c0) arg0 arg1

type Min (a0, b0, c0) arg0 arg1 = Apply (a0, b0, c0) (a0, b0, c0) (Apply (a0, b0, c0) (TyFun (a0, b0, c0) (a0, b0, c0) -> Type) (Min_1627676375Sym0 (a0, b0, c0)) arg0) arg1

type Min (a0, b0, c0, d0) arg0 arg1

type Min (a0, b0, c0, d0) arg0 arg1 = Apply (a0, b0, c0, d0) (a0, b0, c0, d0) (Apply (a0, b0, c0, d0) (TyFun (a0, b0, c0, d0) (a0, b0, c0, d0) -> Type) (Min_1627676375Sym0 (a0, b0, c0, d0)) arg0) arg1

type Min (a0, b0, c0, d0, e0) arg0 arg1

type Min (a0, b0, c0, d0, e0) arg0 arg1 = Apply (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) (Apply (a0, b0, c0, d0, e0) (TyFun (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) -> Type) (Min_1627676375Sym0 (a0, b0, c0, d0, e0)) arg0) arg1

type Min (a0, b0, c0, d0, e0, f0) arg0 arg1

type Min (a0, b0, c0, d0, e0, f0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) (Apply (a0, b0, c0, d0, e0, f0) (TyFun (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) -> Type) (Min_1627676375Sym0 (a0, b0, c0, d0, e0, f0)) arg0) arg1

type Min (a0, b0, c0, d0, e0, f0, g0) arg0 arg1

type Min (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) (Apply (a0, b0, c0, d0, e0, f0, g0) (TyFun (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) -> Type) (Min_1627676375Sym0 (a0, b0, c0, d0, e0, f0, g0)) arg0) arg1

sMin :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MinSym0 a0) t0) t1)

max :: Ord a => a -> a -> a

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

Instances

type Max Bool arg0 arg1

type Max Bool arg0 arg1 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Max_1627676342Sym0 Bool) arg0) arg1

type Max Ordering arg0 arg1

type Max Ordering arg0 arg1 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Max_1627676342Sym0 Ordering) arg0) arg1

type Max Nat arg0 arg1

type Max Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_1627676342Sym0 Nat) arg0) arg1

type Max Symbol arg0 arg1

type Max Symbol arg0 arg1 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Max_1627676342Sym0 Symbol) arg0) arg1

type Max () arg0 arg1

type Max () arg0 arg1 = Apply () () (Apply () (TyFun () () -> Type) (Max_1627676342Sym0 ()) arg0) arg1

type Max Nat a0 a1

type Max Nat a0 a1

type Max [a0] arg0 arg1

type Max [a0] arg0 arg1 = Apply [a0] [a0] (Apply [a0] (TyFun [a0] [a0] -> Type) (Max_1627676342Sym0 [a0]) arg0) arg1

type Max (Maybe a0) arg0 arg1

type Max (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (Maybe a0) (TyFun (Maybe a0) (Maybe a0) -> Type) (Max_1627676342Sym0 (Maybe a0)) arg0) arg1

type Max (NonEmpty a0) arg0 arg1

type Max (NonEmpty a0) arg0 arg1 = Apply (NonEmpty a0) (NonEmpty a0) (Apply (NonEmpty a0) (TyFun (NonEmpty a0) (NonEmpty a0) -> Type) (Max_1627676342Sym0 (NonEmpty a0)) arg0) arg1

type Max (Either a0 b0) arg0 arg1

type Max (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (Either a0 b0) (TyFun (Either a0 b0) (Either a0 b0) -> Type) (Max_1627676342Sym0 (Either a0 b0)) arg0) arg1

type Max (a0, b0) arg0 arg1

type Max (a0, b0) arg0 arg1 = Apply (a0, b0) (a0, b0) (Apply (a0, b0) (TyFun (a0, b0) (a0, b0) -> Type) (Max_1627676342Sym0 (a0, b0)) arg0) arg1

type Max (a0, b0, c0) arg0 arg1

type Max (a0, b0, c0) arg0 arg1 = Apply (a0, b0, c0) (a0, b0, c0) (Apply (a0, b0, c0) (TyFun (a0, b0, c0) (a0, b0, c0) -> Type) (Max_1627676342Sym0 (a0, b0, c0)) arg0) arg1

type Max (a0, b0, c0, d0) arg0 arg1

type Max (a0, b0, c0, d0) arg0 arg1 = Apply (a0, b0, c0, d0) (a0, b0, c0, d0) (Apply (a0, b0, c0, d0) (TyFun (a0, b0, c0, d0) (a0, b0, c0, d0) -> Type) (Max_1627676342Sym0 (a0, b0, c0, d0)) arg0) arg1

type Max (a0, b0, c0, d0, e0) arg0 arg1

type Max (a0, b0, c0, d0, e0) arg0 arg1 = Apply (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) (Apply (a0, b0, c0, d0, e0) (TyFun (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) -> Type) (Max_1627676342Sym0 (a0, b0, c0, d0, e0)) arg0) arg1

type Max (a0, b0, c0, d0, e0, f0) arg0 arg1

type Max (a0, b0, c0, d0, e0, f0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) (Apply (a0, b0, c0, d0, e0, f0) (TyFun (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) -> Type) (Max_1627676342Sym0 (a0, b0, c0, d0, e0, f0)) arg0) arg1

type Max (a0, b0, c0, d0, e0, f0, g0) arg0 arg1

type Max (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) (Apply (a0, b0, c0, d0, e0, f0, g0) (TyFun (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) -> Type) (Max_1627676342Sym0 (a0, b0, c0, d0, e0, f0, g0)) arg0) arg1

sMax :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MaxSym0 a0) t0) t1)

data MinSym0 a1627675388 l0 :: forall a1627675388. TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *) (MinSym0 a1627675388)

Methods

suppressUnusedWarnings :: Proxy (MinSym0 a1627675388) t -> ()

type Apply a1627675388 (TyFun a1627675388 a1627675388 -> Type) (MinSym0 a1627675388) l0

type Apply a1627675388 (TyFun a1627675388 a1627675388 -> Type) (MinSym0 a1627675388) l0 = MinSym1 a1627675388 l0

data MinSym1 a1627675388 l0 l1 :: forall a1627675388. a1627675388 -> TyFun a1627675388 a1627675388 -> *

Instances

SuppressUnusedWarnings (a1627675388 -> TyFun a1627675388 a1627675388 -> *) (MinSym1 a1627675388)

Methods

suppressUnusedWarnings :: Proxy (MinSym1 a1627675388) t -> ()

type Apply a1627675388 a1627675388 (MinSym1 a1627675388 l1) l0

type Apply a1627675388 a1627675388 (MinSym1 a1627675388 l1) l0 = MinSym2 a1627675388 l1 l0

type MinSym2 a1627675388 t0 t1 = Min a1627675388 t0 t1

data MaxSym0 a1627675388 l0 :: forall a1627675388. TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *) (MaxSym0 a1627675388)

Methods

suppressUnusedWarnings :: Proxy (MaxSym0 a1627675388) t -> ()

type Apply a1627675388 (TyFun a1627675388 a1627675388 -> Type) (MaxSym0 a1627675388) l0

type Apply a1627675388 (TyFun a1627675388 a1627675388 -> Type) (MaxSym0 a1627675388) l0 = MaxSym1 a1627675388 l0

data MaxSym1 a1627675388 l0 l1 :: forall a1627675388. a1627675388 -> TyFun a1627675388 a1627675388 -> *

Instances

SuppressUnusedWarnings (a1627675388 -> TyFun a1627675388 a1627675388 -> *) (MaxSym1 a1627675388)

Methods

suppressUnusedWarnings :: Proxy (MaxSym1 a1627675388) t -> ()

type Apply a1627675388 a1627675388 (MaxSym1 a1627675388 l1) l0

type Apply a1627675388 a1627675388 (MaxSym1 a1627675388 l1) l0 = MaxSym2 a1627675388 l1 l0

type MaxSym2 a1627675388 t0 t1 = Max a1627675388 t0 t1

type (:+:) n m = n :+ m infixl 6

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

Instances

type (:+) Nat a b

type (:+) Nat a b = (+) a b

type (:+) Nat a0 a1

type (:+) Nat a0 a1

data a1627810386 :+$ l0 :: forall a1627810386. TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *) ((:+$) a1627810386)

Methods

suppressUnusedWarnings :: Proxy ((:+$) a1627810386) t -> ()

type Apply a1627810386 (TyFun a1627810386 a1627810386 -> Type) ((:+$) a1627810386) l0

type Apply a1627810386 (TyFun a1627810386 a1627810386 -> Type) ((:+$) a1627810386) l0 = (:+$$) a1627810386 l0

data (a1627810386 :+$$ l0) l1 :: forall a1627810386. a1627810386 -> TyFun a1627810386 a1627810386 -> *

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:+$$) a1627810386) t -> ()

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

type Apply a1627810386 a1627810386 ((:+$$) a1627810386 l1) l0 = (:+$$$) a1627810386 l1 l0

type (:+$$$) a1627810386 t0 t1 = (:+) a1627810386 t0 t1

(%+) :: SNat n -> SNat m -> SNat (n :+: m) infixl 6

Addition for singleton numbers.

(%:+) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:+$) a0) t0) t1)

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

Instances

type (:*) Nat a b

type (:*) Nat a b = * a b

type (:*) Nat a0 a1

type (:*) Nat a0 a1

type (:*:) n m = n :* m infixl 7

Type-level multiplication.

data a1627810386 :*$ l0 :: forall a1627810386. TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *) ((:*$) a1627810386)

Methods

suppressUnusedWarnings :: Proxy ((:*$) a1627810386) t -> ()

type Apply a1627810386 (TyFun a1627810386 a1627810386 -> Type) ((:*$) a1627810386) l0

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

data (a1627810386 :*$$ l0) l1 :: forall a1627810386. a1627810386 -> TyFun a1627810386 a1627810386 -> *

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:*$$) a1627810386) t -> ()

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

type Apply a1627810386 a1627810386 ((:*$$) a1627810386 l1) l0 = (:*$$$) a1627810386 l1 l0

type (:*$$$) a1627810386 t0 t1 = (:*) a1627810386 t0 t1

(%:*) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:*$) a0) t0) t1)

(%*) :: SNat n -> SNat m -> SNat (n :*: m) infixl 7

Multiplication for singleton numbers.

type (:-:) n m = n :- m infixl 6

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

Instances

type (:-) Nat a b

type (:-) Nat a b = (-) a b

type (:-) Nat a0 a1

type (:-) Nat a0 a1

type (:**:) n m = n :** m

Type-level exponentiation.

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

Equations

_z_1627480629 :** Z = Apply SSym0 ZSym0

n :** (S m) = Apply (Apply (:*$) (Apply (Apply (:**$) n) m)) n

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

(%**) :: SNat n -> SNat m -> SNat (n :**: m)

Exponentiation for singleton numbers.

data a1627810386 :-$ l0 :: forall a1627810386. TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627810386 (TyFun a1627810386 a1627810386 -> Type) -> *) ((:-$) a1627810386)

Methods

suppressUnusedWarnings :: Proxy ((:-$) a1627810386) t -> ()

type Apply a1627810386 (TyFun a1627810386 a1627810386 -> Type) ((:-$) a1627810386) l0

type Apply a1627810386 (TyFun a1627810386 a1627810386 -> Type) ((:-$) a1627810386) l0 = (:-$$) a1627810386 l0

data (a1627810386 :-$$ l0) l1 :: forall a1627810386. a1627810386 -> TyFun a1627810386 a1627810386 -> *

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:-$$) a1627810386) t -> ()

type Apply a1627810386 a1627810386 ((:-$$) a1627810386 l1) l0

type Apply a1627810386 a1627810386 ((:-$$) a1627810386 l1) l0 = (:-$$$) a1627810386 l1 l0

type (:-$$$) a1627810386 t0 t1 = (:-) a1627810386 t0 t1

(%:-) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:-$) a0) t0) t1)

(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m) infixl 6

Type-level predicate & judgements

data Leq n m where

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m

SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

class n :<= m

Comparison via type-class.

Instances

Z :<= n

(:<=) n m => (S n) :<= (S m)

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

Boolean-valued type-level comparison function.

Equations

Z :<<= _z_1627483216 = TrueSym0

(S _z_1627483219) :<<= Z = FalseSym0

(S n) :<<= (S m) = Apply (Apply (:<<=$) n) m

data (:<<=$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> Type) -> *) (:<<=$)

Methods

suppressUnusedWarnings :: Proxy (:<<=$) t -> ()

type Apply Nat (TyFun Nat Bool -> Type) (:<<=$) l0

type Apply Nat (TyFun Nat Bool -> Type) (:<<=$) l0 = (:<<=$$) l0

data l :<<=$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$)

Methods

suppressUnusedWarnings :: Proxy (:<<=$$) t -> ()

type Apply Nat Bool ((:<<=$$) l1) l0

type Apply Nat Bool ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0

type (:<<=$$$) t t = (:<<=) t t

(%:<<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<<=$) t) t :: Bool)

type LeqInstance n m = Dict (n :<= m)

boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m

boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m

propToClassLeq :: Leq n m -> LeqInstance n m

type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)

propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m

Conversion functions

natToInt :: Integral n => Nat -> n

Convert Nat into normal integers.

intToNat :: (Integral a, Ord a) => a -> Nat

Convert integral numbers into Nat

sNatToInt :: Num n => SNat x -> n

Convert 'SNat n' into normal integers.

Quasi quotes for natural numbers

nat :: QuasiQuoter

Quotesi-quoter for Nat. This can be used for an expression, pattern and type.

for example: sing :: SNat ([nat| 2 |] :+ [nat| 5 |])

snat :: QuasiQuoter

Quotesi-quoter for SNat. This can be used for an expression, pattern and type.

For example: [snat|12|] %+ [snat| 5 |], sing :: [snat| 12 |], f [snat| 12 |] = "hey"

Properties of natural numbers

succCongEq :: (n :=: m) -> S n :=: S m

plusCongR :: SNat n -> (m :=: m') -> (m :+ n) :=: (m' :+ n)

plusCongL :: SNat n -> (m :=: m') -> (n :+ m) :=: (n :+ m')

succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m)

succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)

pluSZR :: SNat n -> (n :+: Z) :=: n

pluSZL :: SNat n -> (Z :+: n) :=: n

eqPreserveSS :: (n :=: m) -> S n :=: S m

plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l)

multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l)

multComm :: SNat n -> SNat m -> (n :* m) :=: (m :* n)

multZL :: SNat m -> (Zero :* m) :=: Zero

multZR :: SNat m -> (m :* Zero) :=: Zero

multOneL :: SNat n -> (One :* n) :=: n

multOneR :: SNat n -> (n :* One) :=: n

snEqZAbsurd :: (S n :=: Z) -> a

succInjective :: (S n :=: S m) -> n :=: m

plusInjectiveL :: SNat n -> SNat m -> SNat l -> ((n :+ m) :=: (n :+ l)) -> m :=: l

plusInjectiveR :: SNat n -> SNat m -> SNat l -> ((n :+ l) :=: (m :+ l)) -> n :=: m

plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l))

multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l))

multCongL :: SNat n -> (m :=: l) -> (n :* m) :=: (n :* l)

multCongR :: SNat n -> (m :=: l) -> (m :* n) :=: (l :* n)

sAndPlusOne :: SNat n -> S n :=: (n :+: One)

plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)

minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l)

minusNilpotent :: SNat n -> (n :-: n) :=: Zero

eqSuccMinus :: (m :<<= n) ~ True => SNat n -> SNat m -> (S n :-: m) :=: S (n :-: m)

plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n

plusMinusEqR :: SNat n -> SNat m -> ((m :+: n) :-: m) :=: n

zAbsorbsMinR :: SNat n -> Min n Z :=: Z

zAbsorbsMinL :: SNat n -> Min Z n :=: Z

pluSSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m)

plusNeutralR :: SNat n -> SNat m -> ((n :+ m) :=: n) -> m :=: Z

plusNeutralL :: SNat n -> SNat m -> ((n :+ m) :=: m) -> n :=: Z

leqRhs :: Leq n m -> SNat m

leqLhs :: Leq n m -> SNat n

minComm :: SNat n -> SNat m -> Min n m :=: Min m n

maxZL :: SNat n -> Max Z n :=: n

maxComm :: SNat n -> SNat m -> Max n m :=: Max m n

maxZR :: SNat n -> Max n Z :=: n

Properties of ordering Leq

leqRefl :: SNat n -> Leq n n

leqSucc :: SNat n -> Leq n (S n)

leqTrans :: Leq n m -> Leq m l -> Leq n l

plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)

plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)

plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)

minLeqL :: SNat n -> SNat m -> Leq (Min n m) n

minLeqR :: SNat n -> SNat m -> Leq (Min n m) m

leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m

maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)

maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)

leqSnZAbsurd :: Leq (S n) Z -> a

leqnZElim :: Leq n Z -> n :=: Z

leqSnLeq :: Leq (S n) m -> Leq n m

leqPred :: Leq (S n) (S m) -> Leq n m

leqSnnAbsurd :: Leq (S n) n -> a

Useful type synonyms and constructors

zero :: Nat

one :: Nat

two :: Nat

three :: Nat

four :: Nat

five :: Nat

six :: Nat

seven :: Nat

eight :: Nat

nine :: Nat

ten :: Nat

eleven :: Nat

twelve :: Nat

thirteen :: Nat

fourteen :: Nat

fifteen :: Nat

sixteen :: Nat

seventeen :: Nat

eighteen :: Nat

nineteen :: Nat

twenty :: Nat

type family Zero :: Nat where ...

Equations

Zero = ZSym0

type family One :: Nat where ...

Equations

One = Apply SSym0 ZeroSym0

type family Two :: Nat where ...

Equations

Two = Apply SSym0 OneSym0

type family Three :: Nat where ...

Equations

Three = Apply SSym0 TwoSym0

type family Four :: Nat where ...

Equations

Four = Apply SSym0 ThreeSym0

type family Five :: Nat where ...

Equations

Five = Apply SSym0 FourSym0

type family Six :: Nat where ...

Equations

Six = Apply SSym0 FiveSym0

type family Seven :: Nat where ...

Equations

Seven = Apply SSym0 SixSym0

type family Eight :: Nat where ...

Equations

Eight = Apply SSym0 SevenSym0

type family Nine :: Nat where ...

Equations

Nine = Apply SSym0 EightSym0

type family Ten :: Nat where ...

Equations

Ten = Apply SSym0 NineSym0

type family Eleven :: Nat where ...

Equations

Eleven = Apply SSym0 TenSym0

type family Twelve :: Nat where ...

Equations

Twelve = Apply SSym0 ElevenSym0

type family Thirteen :: Nat where ...

Equations

Thirteen = Apply SSym0 TwelveSym0

type family Fourteen :: Nat where ...

Equations

Fourteen = Apply SSym0 ThirteenSym0

type family Fifteen :: Nat where ...

Equations

Fifteen = Apply SSym0 FourteenSym0

type family Sixteen :: Nat where ...

Equations

Sixteen = Apply SSym0 FifteenSym0

type family Seventeen :: Nat where ...

Equations

Seventeen = Apply SSym0 SixteenSym0

type family Eighteen :: Nat where ...

Equations

Eighteen = Apply SSym0 SeventeenSym0

type family Nineteen :: Nat where ...

Equations

Nineteen = Apply SSym0 EighteenSym0

type family Twenty :: Nat where ...

Equations

Twenty = Apply SSym0 NineteenSym0

type ZeroSym0 = Zero

type OneSym0 = One

type TwoSym0 = Two

type ThreeSym0 = Three

type FourSym0 = Four

type FiveSym0 = Five

type SixSym0 = Six

type SevenSym0 = Seven

type EightSym0 = Eight

type NineSym0 = Nine

type TenSym0 = Ten

type ElevenSym0 = Eleven

type TwelveSym0 = Twelve

type ThirteenSym0 = Thirteen

type FourteenSym0 = Fourteen

type FifteenSym0 = Fifteen

type SixteenSym0 = Sixteen

type SeventeenSym0 = Seventeen

type EighteenSym0 = Eighteen

type NineteenSym0 = Nineteen

type TwentySym0 = Twenty

sZero :: Sing (ZeroSym0 :: Nat)

sOne :: Sing (OneSym0 :: Nat)

sTwo :: Sing (TwoSym0 :: Nat)

sThree :: Sing (ThreeSym0 :: Nat)

sFour :: Sing (FourSym0 :: Nat)

sFive :: Sing (FiveSym0 :: Nat)

sSix :: Sing (SixSym0 :: Nat)

sSeven :: Sing (SevenSym0 :: Nat)

sEight :: Sing (EightSym0 :: Nat)

sNine :: Sing (NineSym0 :: Nat)

sTen :: Sing (TenSym0 :: Nat)

sEleven :: Sing (ElevenSym0 :: Nat)

sTwelve :: Sing (TwelveSym0 :: Nat)

sThirteen :: Sing (ThirteenSym0 :: Nat)

sFourteen :: Sing (FourteenSym0 :: Nat)

sFifteen :: Sing (FifteenSym0 :: Nat)

sSixteen :: Sing (SixteenSym0 :: Nat)

sSeventeen :: Sing (SeventeenSym0 :: Nat)

sEighteen :: Sing (EighteenSym0 :: Nat)

sNineteen :: Sing (NineteenSym0 :: Nat)

sTwenty :: Sing (TwentySym0 :: Nat)

n0 :: Nat

n1 :: Nat

n2 :: Nat

n3 :: Nat

n4 :: Nat

n5 :: Nat

n6 :: Nat

n7 :: Nat

n8 :: Nat

n9 :: Nat

n10 :: Nat

n11 :: Nat

n12 :: Nat

n13 :: Nat

n14 :: Nat

n15 :: Nat

n16 :: Nat

n17 :: Nat

n18 :: Nat

n19 :: Nat

n20 :: Nat

type family N0 :: Nat where ...

Equations

N0 = ZeroSym0

type family N1 :: Nat where ...

Equations

N1 = OneSym0

type family N2 :: Nat where ...

Equations

N2 = TwoSym0

type family N3 :: Nat where ...

Equations

N3 = ThreeSym0

type family N4 :: Nat where ...

Equations

N4 = FourSym0

type family N5 :: Nat where ...

Equations

N5 = FiveSym0

type family N6 :: Nat where ...

Equations

N6 = SixSym0

type family N7 :: Nat where ...

Equations

N7 = SevenSym0

type family N8 :: Nat where ...

Equations

N8 = EightSym0

type family N9 :: Nat where ...

Equations

N9 = NineSym0

type family N10 :: Nat where ...

Equations

N10 = TenSym0

type family N11 :: Nat where ...

Equations

N11 = ElevenSym0

type family N12 :: Nat where ...

Equations

N12 = TwelveSym0

type family N13 :: Nat where ...

Equations

N13 = ThirteenSym0

type family N14 :: Nat where ...

Equations

N14 = FourteenSym0

type family N15 :: Nat where ...

Equations

N15 = FifteenSym0

type family N16 :: Nat where ...

Equations

N16 = SixteenSym0

type family N17 :: Nat where ...

Equations

N17 = SeventeenSym0

type family N18 :: Nat where ...

Equations

N18 = EighteenSym0

type family N19 :: Nat where ...

Equations

N19 = NineteenSym0

type family N20 :: Nat where ...

Equations

N20 = TwentySym0

type N0Sym0 = N0

type N1Sym0 = N1

type N2Sym0 = N2

type N3Sym0 = N3

type N4Sym0 = N4

type N5Sym0 = N5

type N6Sym0 = N6

type N7Sym0 = N7

type N8Sym0 = N8

type N9Sym0 = N9

type N10Sym0 = N10

type N11Sym0 = N11

type N12Sym0 = N12

type N13Sym0 = N13

type N14Sym0 = N14

type N15Sym0 = N15

type N16Sym0 = N16

type N17Sym0 = N17

type N18Sym0 = N18

type N19Sym0 = N19

type N20Sym0 = N20

sN0 :: Sing (N0Sym0 :: Nat)

sN1 :: Sing (N1Sym0 :: Nat)

sN2 :: Sing (N2Sym0 :: Nat)

sN3 :: Sing (N3Sym0 :: Nat)

sN4 :: Sing (N4Sym0 :: Nat)

sN5 :: Sing (N5Sym0 :: Nat)

sN6 :: Sing (N6Sym0 :: Nat)

sN7 :: Sing (N7Sym0 :: Nat)

sN8 :: Sing (N8Sym0 :: Nat)

sN9 :: Sing (N9Sym0 :: Nat)

sN10 :: Sing (N10Sym0 :: Nat)

sN11 :: Sing (N11Sym0 :: Nat)

sN12 :: Sing (N12Sym0 :: Nat)

sN13 :: Sing (N13Sym0 :: Nat)

sN14 :: Sing (N14Sym0 :: Nat)

sN15 :: Sing (N15Sym0 :: Nat)

sN16 :: Sing (N16Sym0 :: Nat)

sN17 :: Sing (N17Sym0 :: Nat)

sN18 :: Sing (N18Sym0 :: Nat)

sN19 :: Sing (N19Sym0 :: Nat)

sN20 :: Sing (N20Sym0 :: Nat)

Orphan instances

Preorder Nat Leq

Methods

reflexivity :: Sing Leq a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Monomorphicable Nat (Sing Nat)

Associated Types

type MonomorphicRep (Sing Nat) (k1 :: Sing Nat -> *) :: *

Methods

promote :: MonomorphicRep (Sing Nat) k1 -> Monomorphic (Sing Nat) k1

demote :: Monomorphic (Sing Nat) k1 -> MonomorphicRep (Sing Nat) k1