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

Num Nat

Ord Nat

Show Nat

Typeable Nat Z

SingI Nat Z

Preorder Nat Leq

SingKind Nat (KProxy Nat)

SingI Nat n0 => SingI Nat (S n)

Monomorphicable Nat (Sing Nat)

POrd Nat (KProxy Nat)

SEq Nat (KProxy Nat)

PEq Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

Eq (Sing Nat n)

Show (Sing Nat n)

Typeable (Nat -> *) Ordinal

Typeable (Nat -> Nat) S

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

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

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

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

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

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

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

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) MinSym0

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) MaxSym0

SuppressUnusedWarnings (TyFun 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 Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0

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

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

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

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

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

type DemoteRep Nat (KProxy Nat) = Nat

type MonomorphicRep Nat (Sing Nat) = Int

type Compare Nat (S lhs0) Z = GT

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

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

type Apply (TyFun Nat Nat -> *) Nat MinSym0 l0 = MinSym1 l0

type Apply (TyFun Nat Nat -> *) Nat MaxSym0 l0 = MaxSym1 l0

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

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

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

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t

type ZSym0 = Z

Singleton type for Nat.

type SNat z = Sing z

data family Sing a

The singleton kind-indexed data family.

Instances

SDecide k (KProxy k) => TestEquality k (Sing k)

Monomorphicable Nat (Sing Nat)

Eq (Sing Nat n)

Show (Sing Nat n)

data Sing Bool where

• SFalse :: (~) Bool z0 False => Sing Bool z0
• STrue :: (~) Bool z0 True => Sing Bool z0

data Sing Ordering where

• SLT :: (~) Ordering z0 LT => Sing Ordering z0
• SEQ :: (~) Ordering z0 EQ => Sing Ordering z0
• SGT :: (~) Ordering z0 GT => Sing Ordering z0

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

data Sing () where

• STuple0 :: (~) () z0 () => Sing () z0

data Sing Nat where

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

type MonomorphicRep Nat (Sing Nat) = Int

data Sing [a0] where

• SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0
• SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0

data Sing (Maybe a0) where

• SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0
• SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0

data Sing (TyFun k1 k2 -> *) = SLambda {

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

}

data Sing (Either a0 b0) where

• SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0
• SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0

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

• STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0

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

• STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0

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

• STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0

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

• STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0

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

• STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

Smart constructors

WARNING: Smart constructors are deprecated as of singletons 0.10, so these are provided only for backward compatibility.

sZ :: SNat Z

Deprecated: Smart constructors are no longer needed in singletons; Use SS or SZ instead.

sS :: SNat n -> SNat (S n)

Deprecated: Smart constructors are no longer needed in singletons; Use SS or SZ instead.

Arithmetic functions and their singletons.

min :: Nat -> Nat -> Nat

type family Min a a :: Nat

Equations

Min Z Z = ZSym0

Min Z (S z) = ZSym0

Min (S z) Z = ZSym0

Min (S m) (S n) = Apply SSym0 (Apply (Apply MinSym0 m) n)

sMin :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

max :: Nat -> Nat -> Nat

type family Max a a :: Nat

Equations

Max Z Z = ZSym0

Max Z (S n) = Apply SSym0 n

Max (S n) Z = Apply SSym0 n

Max (S n) (S m) = Apply SSym0 (Apply (Apply MaxSym0 n) m)

sMax :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

data MinSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) MinSym0

type Apply (TyFun Nat Nat -> *) Nat MinSym0 l0 = MinSym1 l0

data MinSym1 l l

Instances

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

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

type MinSym2 t t = Min t t

data MaxSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) MaxSym0

type Apply (TyFun Nat Nat -> *) Nat MaxSym0 l0 = MaxSym1 l0

data MaxSym1 l l

Instances

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

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

type MaxSym2 t t = Max t t

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

type family a :+ a :: Nat infixl 6

Equations

Z :+ n = n

(S m) :+ n = Apply SSym0 (Apply (Apply (:+$) m) n)

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 = (:+$$$) l1 l0

type (:+$$$) t t = (:+) t t

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

Addition for singleton numbers.

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

type family a :* a :: Nat infixl 7

Equations

Z :* z = ZSym0

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

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

Type-level multiplication.

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 = (:*$$$) l1 l0

type (:*$$$) t t = (:*) t t

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

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

Multiplication for singleton numbers.

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

type family a :- a :: Nat

Equations

n :- Z = n

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

Z :- (S z) = ZSym0

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

Type-level exponentiation.

type family a :** a :: Nat

Equations

n :** 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)

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

Exponentiation for singleton numbers.

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 = (:-$$$) l1 l0

type (:-$$$) t t = (:-) t t

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

(%-) :: ((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)

Instances

Preorder Nat Leq

class n :<= m

Comparison via type-class.

Instances

Z :<= n

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

type family a :<<= a :: Bool

Boolean-valued type-level comparison function.

Equations

Z :<<= z = TrueSym0

(S z) :<<= Z = FalseSym0

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

data (:<<=$) l

Instances

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

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

data l :<<=$$ l

Instances

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

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

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

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

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 :: 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 Zero = (ZSym0 :: Nat)

type One = (Apply SSym0 ZeroSym0 :: Nat)

type Two = (Apply SSym0 OneSym0 :: Nat)

type Three = (Apply SSym0 TwoSym0 :: Nat)

type Four = (Apply SSym0 ThreeSym0 :: Nat)

type Five = (Apply SSym0 FourSym0 :: Nat)

type Six = (Apply SSym0 FiveSym0 :: Nat)

type Seven = (Apply SSym0 SixSym0 :: Nat)

type Eight = (Apply SSym0 SevenSym0 :: Nat)

type Nine = (Apply SSym0 EightSym0 :: Nat)

type Ten = (Apply SSym0 NineSym0 :: Nat)

type Eleven = (Apply SSym0 TenSym0 :: Nat)

type Twelve = (Apply SSym0 ElevenSym0 :: Nat)

type Thirteen = (Apply SSym0 TwelveSym0 :: Nat)

type Fourteen = (Apply SSym0 ThirteenSym0 :: Nat)

type Fifteen = (Apply SSym0 FourteenSym0 :: Nat)

type Sixteen = (Apply SSym0 FifteenSym0 :: Nat)

type Seventeen = (Apply SSym0 SixteenSym0 :: Nat)

type Eighteen = (Apply SSym0 SeventeenSym0 :: Nat)

type Nineteen = (Apply SSym0 EighteenSym0 :: Nat)

type Twenty = (Apply SSym0 NineteenSym0 :: Nat)

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

sOne :: Sing OneSym0

sTwo :: Sing TwoSym0

sThree :: Sing ThreeSym0

sFour :: Sing FourSym0

sFive :: Sing FiveSym0

sSix :: Sing SixSym0

sSeven :: Sing SevenSym0

sEight :: Sing EightSym0

sNine :: Sing NineSym0

sTen :: Sing TenSym0

sEleven :: Sing ElevenSym0

sTwelve :: Sing TwelveSym0

sThirteen :: Sing ThirteenSym0

sFourteen :: Sing FourteenSym0

sFifteen :: Sing FifteenSym0

sSixteen :: Sing SixteenSym0

sSeventeen :: Sing SeventeenSym0

sEighteen :: Sing EighteenSym0

sNineteen :: Sing NineteenSym0

sTwenty :: Sing TwentySym0

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 N0 = (ZeroSym0 :: Nat)

type N1 = (OneSym0 :: Nat)

type N2 = (TwoSym0 :: Nat)

type N3 = (ThreeSym0 :: Nat)

type N4 = (FourSym0 :: Nat)

type N5 = (FiveSym0 :: Nat)

type N6 = (SixSym0 :: Nat)

type N7 = (SevenSym0 :: Nat)

type N8 = (EightSym0 :: Nat)

type N9 = (NineSym0 :: Nat)

type N10 = (TenSym0 :: Nat)

type N11 = (ElevenSym0 :: Nat)

type N12 = (TwelveSym0 :: Nat)

type N13 = (ThirteenSym0 :: Nat)

type N14 = (FourteenSym0 :: Nat)

type N15 = (FifteenSym0 :: Nat)

type N16 = (SixteenSym0 :: Nat)

type N17 = (SeventeenSym0 :: Nat)

type N18 = (EighteenSym0 :: Nat)

type N19 = (NineteenSym0 :: Nat)

type N20 = (TwentySym0 :: Nat)

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

sN1 :: Sing N1Sym0

sN2 :: Sing N2Sym0

sN3 :: Sing N3Sym0

sN4 :: Sing N4Sym0

sN5 :: Sing N5Sym0

sN6 :: Sing N6Sym0

sN7 :: Sing N7Sym0

sN8 :: Sing N8Sym0

sN9 :: Sing N9Sym0

sN10 :: Sing N10Sym0

sN11 :: Sing N11Sym0

sN12 :: Sing N12Sym0

sN13 :: Sing N13Sym0

sN14 :: Sing N14Sym0

sN15 :: Sing N15Sym0

sN16 :: Sing N16Sym0

sN17 :: Sing N17Sym0

sN18 :: Sing N18Sym0

sN19 :: Sing N19Sym0

sN20 :: Sing N20Sym0