lol-0.4.0.0: A library for lattice cryptography.

Crypto.Lol.Factored

Description

$$\def\lcm{\text{lcm}}$$

This module defines types and operations for type-level representation and manipulation of natural numbers, as represented by their prime-power factorizations. It relies on Template Haskell, so parts of the documentation may be difficult to read. See source-level comments for further details.

Synopsis

# Factored natural numbers

reifyFact :: Int -> (forall m. SFactored m -> a) -> a Source #

Reify a Factored as a singleton.

reifyFactI :: Int -> (forall m proxy. Fact m => proxy m -> a) -> a Source #

Reify a Factored for a Fact constraint.

data Factored Source #

Instances

 Source # Methods Source # MethodsshowList :: [Factored] -> ShowS # (Fact m, C i) => Reflects Factored m i Source # Methodsvalue :: Tagged m i i Source # Source # Methods(%:==) :: Sing (KProxy Factored) a -> Sing (KProxy Factored) b -> Sing Bool ((KProxy Factored :== a) b) #(%:/=) :: Sing (KProxy Factored) a -> Sing (KProxy Factored) b -> Sing Bool ((KProxy Factored :/= a) b) # Source # Associated Typestype ((KProxy Factored) :== (x :: KProxy Factored)) (y :: KProxy Factored) :: Bool #type ((KProxy Factored) :/= (x :: KProxy Factored)) (y :: KProxy Factored) :: Bool # Source # Methods(%~) :: Sing (KProxy Factored) a -> Sing (KProxy Factored) b -> Decision ((KProxy Factored :~: a) b) # Source # Associated Typestype DemoteRep (KProxy Factored) (kparam :: KProxy (KProxy Factored)) :: * # MethodsfromSing :: Sing (KProxy Factored) a -> DemoteRep (KProxy Factored) kparam #toSing :: DemoteRep (KProxy Factored) kparam -> SomeSing (KProxy Factored) kparam # data Sing Factored Source # data Sing Factored whereSF :: Sing Factored z type (:/=) Factored x y Source # type (:/=) Factored x y = Not ((:==) Factored x y) type (:==) Factored a0 b0 Source # type (:==) Factored a0 b0 Source #

type Fact m = SingI m Source #

Kind-restricted synonym for SingI.

Template Haskell splice for the Factored type corresponding to a given positive integer. Factors its argument using a naive trial-division algorithm with primes, so should only be used on small-to-moderate-sized arguments (any reasonable cyclotomic index should be OK).

Template Haskell splice that defines the Factored type synonym F$$n$$ for a positive integer $$n$$.

# Prime powers

reifyPPow :: (Int, Int) -> (forall pp. SPrimePower pp -> a) -> a Source #

Reify a PrimePower as a singleton.

reifyPPowI :: (Int, Int) -> (forall pp proxy. PPow pp => proxy pp -> a) -> a Source #

Reify a PrimePower for a PPow constraint.

Instances

 Source # Methods Source # MethodsshowList :: [PrimePower] -> ShowS # (PPow pp, C i) => Reflects PrimePower pp i Source # Methodsvalue :: Tagged pp i i Source # Source # Methods(%:==) :: Sing (KProxy PrimePower) a -> Sing (KProxy PrimePower) b -> Sing Bool ((KProxy PrimePower :== a) b) #(%:/=) :: Sing (KProxy PrimePower) a -> Sing (KProxy PrimePower) b -> Sing Bool ((KProxy PrimePower :/= a) b) # Source # Associated Typestype ((KProxy PrimePower) :== (x :: KProxy PrimePower)) (y :: KProxy PrimePower) :: Bool #type ((KProxy PrimePower) :/= (x :: KProxy PrimePower)) (y :: KProxy PrimePower) :: Bool # Source # Methods(%~) :: Sing (KProxy PrimePower) a -> Sing (KProxy PrimePower) b -> Decision ((KProxy PrimePower :~: a) b) # Source # Associated Typestype DemoteRep (KProxy PrimePower) (kparam :: KProxy (KProxy PrimePower)) :: * # MethodsfromSing :: Sing (KProxy PrimePower) a -> DemoteRep (KProxy PrimePower) kparam #toSing :: DemoteRep (KProxy PrimePower) kparam -> SomeSing (KProxy PrimePower) kparam # (PPow pp, (~) * zq (ZqBasic PrimePower pp z), PrimeField (ZpOf zq), Ring zq) => ZPP (ZqBasic PrimePower pp z) Source # Associated Typestype ZpOf (ZqBasic PrimePower pp z) :: * Source # MethodsliftZp :: ZpOf (ZqBasic PrimePower pp z) -> ZqBasic PrimePower pp z Source # data Sing PrimePower Source # data Sing PrimePower whereSPP :: Sing PrimePower z type (:/=) PrimePower x y Source # type (:/=) PrimePower x y = Not ((:==) PrimePower x y) type (:==) PrimePower a0 b0 Source # type (:==) PrimePower a0 b0 Source # type ZpOf (ZqBasic PrimePower pp z) Source # type ZpOf (ZqBasic PrimePower pp z) = ZqBasic PrimeBin (PrimePP pp) z

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

The singleton kind-indexed data family.

Instances

 data Sing Bool data Sing Bool whereSFalse :: Sing Bool z0STrue :: Sing Bool z0 data Sing Ordering data Sing Ordering whereSLT :: Sing Ordering z0SEQ :: Sing Ordering z0SGT :: Sing Ordering z0 data Sing Nat data Sing Nat whereSNat :: Sing Nat n data Sing Symbol data Sing Symbol whereSSym :: Sing Symbol n data Sing () data Sing () whereSTuple0 :: Sing () z0 data Sing Pos # data Sing Pos whereSO :: Sing Pos zSS :: Sing Pos z data Sing Bin # data Sing Bin whereSB1 :: Sing Bin zSD0 :: Sing Bin zSD1 :: Sing Bin z data Sing PrimeBin # data Sing PrimeBin whereSP :: Sing PrimeBin z data Sing PrimePower # data Sing PrimePower whereSPP :: Sing PrimePower z data Sing Factored # data Sing Factored whereSF :: Sing Factored z data Sing [a0] data Sing [a0] whereSNil :: Sing [a0] z0SCons :: Sing [a0] z0 data Sing (Maybe a0) data Sing (Maybe a0) whereSNothing :: Sing (Maybe a0) z0SJust :: Sing (Maybe a0) z0 data Sing (TyFun k1 k2 -> *) data Sing (TyFun k1 k2 -> *) = SLambda {applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)} data Sing (Either a0 b0) data Sing (Either a0 b0) whereSLeft :: Sing (Either a0 b0) z0SRight :: Sing (Either a0 b0) z0 data Sing (a0, b0) data Sing (a0, b0) whereSTuple2 :: Sing (a0, b0) z0 data Sing (a0, b0, c0) data Sing (a0, b0, c0) whereSTuple3 :: Sing (a0, b0, c0) z0 data Sing (a0, b0, c0, d0) data Sing (a0, b0, c0, d0) whereSTuple4 :: Sing (a0, b0, c0, d0) z0 data Sing (a0, b0, c0, d0, e0) data Sing (a0, b0, c0, d0, e0) whereSTuple5 :: Sing (a0, b0, c0, d0, e0) z0 data Sing (a0, b0, c0, d0, e0, f0) data Sing (a0, b0, c0, d0, e0, f0) whereSTuple6 :: 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) whereSTuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type PPow pp = SingI pp Source #

Kind-restricted synonym for SingI.

Template Haskell splice for the PrimePower type corresponding to a given PP. (Calls pType on the first component of its argument, so should only be used on small-to-moderate-sized numbers.) This is the preferred (and only) way of constructing a concrete PrimePower type.

Template Haskell splice that defines the PrimePower type synonym PP$$n$$, where $$n=p^e$$.

# Primes

reifyPrime :: Int -> (forall p. SPrimeBin p -> a) -> a Source #

Reify a PrimeBin as a singleton.

reifyPrimeI :: Int -> (forall p proxy. Prime p => proxy p -> a) -> a Source #

Reify a PrimeBin for a Prime constraint.

data PrimeBin Source #

Instances

 Source # Methods Source # Methods(<) :: PrimeBin -> PrimeBin -> Bool #(>) :: PrimeBin -> PrimeBin -> Bool # Source # MethodsshowList :: [PrimeBin] -> ShowS # (Prime p, C i) => Reflects PrimeBin p i Source # Methodsvalue :: Tagged p i i Source # Source # Associated Typestype Compare (KProxy PrimeBin) (arg0 :: KProxy PrimeBin) (arg1 :: KProxy PrimeBin) :: Ordering #type ((KProxy PrimeBin) :< (arg0 :: KProxy PrimeBin)) (arg1 :: KProxy PrimeBin) :: Bool #type ((KProxy PrimeBin) :<= (arg0 :: KProxy PrimeBin)) (arg1 :: KProxy PrimeBin) :: Bool #type ((KProxy PrimeBin) :> (arg0 :: KProxy PrimeBin)) (arg1 :: KProxy PrimeBin) :: Bool #type ((KProxy PrimeBin) :>= (arg0 :: KProxy PrimeBin)) (arg1 :: KProxy PrimeBin) :: Bool #type Max (KProxy PrimeBin) (arg0 :: KProxy PrimeBin) (arg1 :: KProxy PrimeBin) :: a0 #type Min (KProxy PrimeBin) (arg0 :: KProxy PrimeBin) (arg1 :: KProxy PrimeBin) :: a0 # Source # MethodssCompare :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing Ordering (Apply (KProxy PrimeBin) Ordering (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) Ordering -> Type) (CompareSym0 (KProxy PrimeBin)) t0) t1) #(%:<) :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing Bool (Apply (KProxy PrimeBin) Bool (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) Bool -> Type) ((:<$) (KProxy PrimeBin)) t0) t1) #(%:<=) :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing Bool (Apply (KProxy PrimeBin) Bool (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) Bool -> Type) ((:<=$) (KProxy PrimeBin)) t0) t1) #(%:>) :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing Bool (Apply (KProxy PrimeBin) Bool (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) Bool -> Type) ((:>$) (KProxy PrimeBin)) t0) t1) #(%:>=) :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing Bool (Apply (KProxy PrimeBin) Bool (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) Bool -> Type) ((:>=$) (KProxy PrimeBin)) t0) t1) #sMax :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing (KProxy PrimeBin) (Apply (KProxy PrimeBin) (KProxy PrimeBin) (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) (KProxy PrimeBin) -> Type) (MaxSym0 (KProxy PrimeBin)) t0) t1) #sMin :: Sing (KProxy PrimeBin) t0 -> Sing (KProxy PrimeBin) t1 -> Sing (KProxy PrimeBin) (Apply (KProxy PrimeBin) (KProxy PrimeBin) (Apply (KProxy PrimeBin) (TyFun (KProxy PrimeBin) (KProxy PrimeBin) -> Type) (MinSym0 (KProxy PrimeBin)) t0) t1) # Source # Methods(%:==) :: Sing (KProxy PrimeBin) a -> Sing (KProxy PrimeBin) b -> Sing Bool ((KProxy PrimeBin :== a) b) #(%:/=) :: Sing (KProxy PrimeBin) a -> Sing (KProxy PrimeBin) b -> Sing Bool ((KProxy PrimeBin :/= a) b) # Source # Associated Typestype ((KProxy PrimeBin) :== (x :: KProxy PrimeBin)) (y :: KProxy PrimeBin) :: Bool #type ((KProxy PrimeBin) :/= (x :: KProxy PrimeBin)) (y :: KProxy PrimeBin) :: Bool # Source # Methods(%~) :: Sing (KProxy PrimeBin) a -> Sing (KProxy PrimeBin) b -> Decision ((KProxy PrimeBin :~: a) b) # Source # Associated Typestype DemoteRep (KProxy PrimeBin) (kparam :: KProxy (KProxy PrimeBin)) :: * # MethodsfromSing :: Sing (KProxy PrimeBin) a -> DemoteRep (KProxy PrimeBin) kparam #toSing :: DemoteRep (KProxy PrimeBin) kparam -> SomeSing (KProxy PrimeBin) kparam # data Sing PrimeBin Source # data Sing PrimeBin whereSP :: Sing PrimeBin z type Min PrimeBin arg0 arg1 Source # type Min PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Min_1627682018Sym0 PrimeBin) arg0) arg1 type Max PrimeBin arg0 arg1 Source # type Max PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Max_1627681985Sym0 PrimeBin) arg0) arg1 type (:>=) PrimeBin arg0 arg1 Source # type (:>=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627681952Sym0 PrimeBin) arg0) arg1 type (:>) PrimeBin arg0 arg1 Source # type (:>) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627681919Sym0 PrimeBin) arg0) arg1 type (:<=) PrimeBin arg0 arg1 Source # type (:<=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627681886Sym0 PrimeBin) arg0) arg1 type (:<) PrimeBin arg0 arg1 Source # type (:<) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627681853Sym0 PrimeBin) arg0) arg1 type Compare PrimeBin a0 a1 Source # type Compare PrimeBin a0 a1 type (:/=) PrimeBin x y Source # type (:/=) PrimeBin x y = Not ((:==) PrimeBin x y) type (:==) PrimeBin a0 b0 Source # type (:==) PrimeBin a0 b0 Source #

type Prime p = SingI p Source #

Kind-restricted synonym for SingI.

Template Haskell splice for the PrimeBin type corresponding to a given positive prime integer. (Uses prime to enforce primality of the base, so should only be used on small-to-moderate-sized arguments.) This is the preferred (and only) way of constructing a concrete PrimeBin type (and is used to define the Prime$$p$$ type synonyms).

Template Haskell splice that defines the PrimeBin type synonym Prime$$p$$ for a positive prime integer $$p$$.

# Constructors

sPToPP :: forall t. Sing t -> Sing (Apply PToPPSym0 t :: PrimePower) Source #

type family PToPP (a :: PrimeBin) :: PrimePower where ... Source #

Equations

 PToPP p = Apply PPSym0 (Apply (Apply Tuple2Sym0 p) OSym0)

sPpToF :: forall t. Sing t -> Sing (Apply PpToFSym0 t :: Factored) Source #

type family PpToF (a :: PrimePower) :: Factored where ... Source #

Equations

 PpToF pp = Apply FSym0 (Apply (Apply (:$) pp) '[]) sPToF :: forall t. Sing t -> Sing (Apply PToFSym0 t :: Factored) Source # type family PToF (a :: PrimeBin) :: Factored where ... Source # Equations  PToF a_1627779347 = Apply (Apply (Apply (:.$) PpToFSym0) PToPPSym0) a_1627779347

# Unwrappers

sUnF :: forall t. Sing t -> Sing (Apply UnFSym0 t :: [PrimePower]) Source #

type family UnF (a :: Factored) :: [PrimePower] where ... Source #

Equations

 UnF (F pps) = pps

sUnPP :: forall t. Sing t -> Sing (Apply UnPPSym0 t :: (PrimeBin, Pos)) Source #

type family UnPP (a :: PrimePower) :: (PrimeBin, Pos) where ... Source #

Equations

 UnPP (PP pp) = pp

type family PrimePP (a :: PrimePower) :: PrimeBin where ... Source #

Equations

 PrimePP a_1627768490 = Apply (Apply (Apply (:.$) FstSym0) UnPPSym0) a_1627768490 type family ExponentPP (a :: PrimePower) :: Pos where ... Source # Equations  ExponentPP a_1627768497 = Apply (Apply (Apply (:.$) SndSym0) UnPPSym0) a_1627768497

# Arithmetic operations

type family FPPMul (a :: PrimePower) (a :: Factored) :: Factored where ... Source #

Equations

 FPPMul pp (F pps) = Apply FSym0 (Apply (Apply PpMulSym0 pp) pps)

type family FMul (a :: Factored) (a :: Factored) :: Factored where ... Source #

Equations

 FMul (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsMulSym0 pps1) pps2)

type * a b = FMul a b Source #

Type (family) synonym for multiplication of Factored types.

type family FDivides (a :: Factored) (a :: Factored) :: Bool where ... Source #

Equations

 FDivides (F pps1) (F pps2) = Apply (Apply PpsDividesSym0 pps1) pps2

type Divides m m' = (Fact m, Fact m', FDivides m m' ~ True) Source #

Constraint synonym for divisibility of Factored types.

type family FDiv (a :: Factored) (a :: Factored) :: Factored where ... Source #

Equations

 FDiv (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsDivSym0 pps1) pps2)

type (/) a b = FDiv a b Source #

Type (family) synonym for division of Factored types.

type family FGCD (a :: Factored) (a :: Factored) :: Factored where ... Source #

Equations

 FGCD (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsGCDSym0 pps1) pps2)

type family FLCM (a :: Factored) (a :: Factored) :: Factored where ... Source #

Equations

 FLCM (F pps1) (F pps2) = Apply FSym0 (Apply (Apply PpsLCMSym0 pps1) pps2)

type Coprime m m' = FGCD m m' ~ F1 Source #

Constraint synonym for coprimality of Factored types.

type family FOddRadical (a :: Factored) :: Factored where ... Source #

Equations

type family PFree (a :: PrimeBin) (a :: Factored) :: Factored where ... Source #

Equations

 PFree p (F pps) = Apply FSym0 (Apply (Let1627801785GoSym2 p pps) pps)

# Convenient reflections

ppsFact :: forall m. Fact m => Tagged m [PP] Source #

Value-level prime-power factorization tagged by a Factored type.

The value of a Factored type.

The totient of a Factored type's value.

The "hat" of a Factored type's value: $$\hat{m} = \begin{cases} m & \mbox{if } m \text{ is odd} \\ m/2 & \text{otherwise} \end{cases}$$.

The radical (product of prime divisors) of a Factored type.

The odd radical (product of odd prime divisors) of a Factored type.

ppPPow :: forall pp. PPow pp => Tagged pp PP Source #

Reflect a PrimePower type to a PP value.

primePPow :: PPow pp => Tagged pp Int Source #

Reflect the prime component of a PrimePower type.

exponentPPow :: PPow pp => Tagged pp Int Source #

Reflect the exponent component of a PrimePower type.

valuePPow :: PPow pp => Tagged pp Int Source #

The value of a PrimePower type.

totientPPow :: PPow pp => Tagged pp Int Source #

The totient of a PrimePower type's value.

valuePrime :: forall p. Prime p => Tagged p Int Source #

The value of a PrimeBin type.

# Number-theoretic laws

transDivides :: forall k l m. Proxy k -> Proxy l -> Proxy m -> (k Divides l, l Divides m) :- (k Divides m) Source #

Entails constraint for transitivity of division, i.e. if $$k \mid l$$ and $$l \mid m$$, then $$k \mid m$$.

gcdDivides :: forall m1 m2 g. Proxy m1 -> Proxy m2 -> (Fact m1, Fact m2, g ~ FGCD m1 m2) :- (g Divides m1, g Divides m2) Source #

Entailment for divisibility by GCD: if $$g=\gcd(m_1,m_2)$$ then $$g \mid m_1$$ and $$g \mid m_2$$.

lcmDivides :: forall m1 m2 l. Proxy m1 -> Proxy m2 -> (Fact m1, Fact m2, l ~ FLCM m1 m2) :- (m1 Divides l, m2 Divides l) Source #

Entailment for LCM divisibility: if $$l=\lcm(m_1,m_2)$$ then $$m_1 \mid l$$ and $$m_2 \mid l$$.

lcm2Divides :: forall m1 m2 l m. Proxy m1 -> Proxy m2 -> Proxy m -> (m1 Divides m, m2 Divides m, l ~ FLCM m1 m2) :- (m1 Divides l, m2 Divides l, FLCM m1 m2 Divides m) Source #

Entailment for LCM divisibility: the LCM of two divisors of $$m$$ also divides $$m$$.

pSplitTheorems :: forall p m f. Proxy p -> Proxy m -> (Prime p, Fact m, f ~ PFree p m) :- (f Divides m, Coprime (PToF p) f) Source #

Entailment for $$p$$-free division: if $$f$$ is $$m$$ after removing all $$p$$-factors, then $$f \mid m$$ and $$\gcd(f,p)=1$$.

pFreeDivides :: forall p m m'. Proxy p -> Proxy m -> Proxy m' -> (Prime p, m Divides m') :- (PFree p m Divides PFree p m') Source #

Entailment for $$p$$-free division: if $$m \mid m'$$, then $$\text{p-free}(m) \mid \text{p-free}(m')$$.

(\\) :: a => (b -> r) -> (:-) a b -> r infixl 1 #

Given that a :- b, derive something that needs a context b, using the context a

# Utility operations on prime powers

valueHat :: Integral i => i -> i Source #

Return $$m$$ if $$m$$ is odd, and $$m/2$$ otherwise.

type PP = (Int, Int) Source #

Type synonym for (prime, exponent) pair.

Conversion.

The value of a prime power.

Totient of a prime power.

The radical of a prime power.

The odd radical of a prime power.

valuePPs :: [PP] -> Int Source #

Product of values of individual PPs

totientPPs :: [PP] -> Int Source #

Product of totients of individual PPs

radicalPPs :: [PP] -> Int Source #

Product of radicals of individual PPs

oddRadicalPPs :: [PP] -> Int Source #

Product of odd radicals of individual PPs

# Positive naturals in Peano representation

data Pos Source #

Constructors

 O S Pos

Instances

 Source # Methods(==) :: Pos -> Pos -> Bool #(/=) :: Pos -> Pos -> Bool # Source # Methodscompare :: Pos -> Pos -> Ordering #(<) :: Pos -> Pos -> Bool #(<=) :: Pos -> Pos -> Bool #(>) :: Pos -> Pos -> Bool #(>=) :: Pos -> Pos -> Bool #max :: Pos -> Pos -> Pos #min :: Pos -> Pos -> Pos # Source # MethodsshowsPrec :: Int -> Pos -> ShowS #show :: Pos -> String #showList :: [Pos] -> ShowS # Source # Methodssing :: Sing O a # Source # Associated Typestype Compare (KProxy Pos) (arg0 :: KProxy Pos) (arg1 :: KProxy Pos) :: Ordering #type ((KProxy Pos) :< (arg0 :: KProxy Pos)) (arg1 :: KProxy Pos) :: Bool #type ((KProxy Pos) :<= (arg0 :: KProxy Pos)) (arg1 :: KProxy Pos) :: Bool #type ((KProxy Pos) :> (arg0 :: KProxy Pos)) (arg1 :: KProxy Pos) :: Bool #type ((KProxy Pos) :>= (arg0 :: KProxy Pos)) (arg1 :: KProxy Pos) :: Bool #type Max (KProxy Pos) (arg0 :: KProxy Pos) (arg1 :: KProxy Pos) :: a0 #type Min (KProxy Pos) (arg0 :: KProxy Pos) (arg1 :: KProxy Pos) :: a0 # Source # MethodssCompare :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing Ordering (Apply (KProxy Pos) Ordering (Apply (KProxy Pos) (TyFun (KProxy Pos) Ordering -> Type) (CompareSym0 (KProxy Pos)) t0) t1) #(%:<) :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing Bool (Apply (KProxy Pos) Bool (Apply (KProxy Pos) (TyFun (KProxy Pos) Bool -> Type) ((:<$) (KProxy Pos)) t0) t1) #(%:<=) :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing Bool (Apply (KProxy Pos) Bool (Apply (KProxy Pos) (TyFun (KProxy Pos) Bool -> Type) ((:<=$) (KProxy Pos)) t0) t1) #(%:>) :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing Bool (Apply (KProxy Pos) Bool (Apply (KProxy Pos) (TyFun (KProxy Pos) Bool -> Type) ((:>$) (KProxy Pos)) t0) t1) #(%:>=) :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing Bool (Apply (KProxy Pos) Bool (Apply (KProxy Pos) (TyFun (KProxy Pos) Bool -> Type) ((:>=$) (KProxy Pos)) t0) t1) #sMax :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing (KProxy Pos) (Apply (KProxy Pos) (KProxy Pos) (Apply (KProxy Pos) (TyFun (KProxy Pos) (KProxy Pos) -> Type) (MaxSym0 (KProxy Pos)) t0) t1) #sMin :: Sing (KProxy Pos) t0 -> Sing (KProxy Pos) t1 -> Sing (KProxy Pos) (Apply (KProxy Pos) (KProxy Pos) (Apply (KProxy Pos) (TyFun (KProxy Pos) (KProxy Pos) -> Type) (MinSym0 (KProxy Pos)) t0) t1) # Source # Methods(%:==) :: Sing (KProxy Pos) a -> Sing (KProxy Pos) b -> Sing Bool ((KProxy Pos :== a) b) #(%:/=) :: Sing (KProxy Pos) a -> Sing (KProxy Pos) b -> Sing Bool ((KProxy Pos :/= a) b) # Source # Associated Typestype ((KProxy Pos) :== (x :: KProxy Pos)) (y :: KProxy Pos) :: Bool #type ((KProxy Pos) :/= (x :: KProxy Pos)) (y :: KProxy Pos) :: Bool # Source # Methods(%~) :: Sing (KProxy Pos) a -> Sing (KProxy Pos) b -> Decision ((KProxy Pos :~: a) b) # SingI Pos n0 => SingI Pos (S n0) Source # Methodssing :: Sing (S n0) a # Source # Associated Typestype DemoteRep (KProxy Pos) (kparam :: KProxy (KProxy Pos)) :: * # MethodsfromSing :: Sing (KProxy Pos) a -> DemoteRep (KProxy Pos) kparam #toSing :: DemoteRep (KProxy Pos) kparam -> SomeSing (KProxy Pos) kparam # Source # Methods Source # Methods Source # Methods Source # Methods Source # MethodssuppressUnusedWarnings :: Proxy SSym0 t -> () # data Sing Pos Source # data Sing Pos whereSO :: Sing Pos zSS :: Sing Pos z type Min Pos arg0 arg1 Source # type Min Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Min_1627682018Sym0 Pos) arg0) arg1 type Max Pos arg0 arg1 Source # type Max Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Max_1627681985Sym0 Pos) arg0) arg1 type (:>=) Pos arg0 arg1 Source # type (:>=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627681952Sym0 Pos) arg0) arg1 type (:>) Pos arg0 arg1 Source # type (:>) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627681919Sym0 Pos) arg0) arg1 type (:<=) Pos arg0 arg1 Source # type (:<=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627681886Sym0 Pos) arg0) arg1 type (:<) Pos arg0 arg1 Source # type (:<) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627681853Sym0 Pos) arg0) arg1 type Compare Pos a0 a1 Source # type Compare Pos a0 a1 type (:/=) Pos x y Source # type (:/=) Pos x y = Not ((:==) Pos x y) type (:==) Pos a0 b0 Source # type (:==) Pos a0 b0 type Apply Pos Pos SSym0 l0 Source # type Apply Pos Pos SSym0 l0 = SSym1 l0 type Apply Pos Pos (AddPosSym1 l1) l0 Source # type Apply Pos Pos (AddPosSym1 l1) l0 type Apply Pos Pos (SubPosSym1 l1) l0 Source # type Apply Pos Pos (SubPosSym1 l1) l0 type DemoteRep Pos (KProxy Pos) Source # type DemoteRep Pos (KProxy Pos) = Pos type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 Source # type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 = AddPosSym1 l0 type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 Source # type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 = SubPosSym1 l0

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

The singleton kind-indexed data family.

Instances

 data Sing Bool data Sing Bool whereSFalse :: Sing Bool z0STrue :: Sing Bool z0 data Sing Ordering data Sing Ordering whereSLT :: Sing Ordering z0SEQ :: Sing Ordering z0SGT :: Sing Ordering z0 data Sing Nat data Sing Nat whereSNat :: Sing Nat n data Sing Symbol data Sing Symbol whereSSym :: Sing Symbol n data Sing () data Sing () whereSTuple0 :: Sing () z0 data Sing Pos # data Sing Pos whereSO :: Sing Pos zSS :: Sing Pos z data Sing Bin # data Sing Bin whereSB1 :: Sing Bin zSD0 :: Sing Bin zSD1 :: Sing Bin z data Sing PrimeBin # data Sing PrimeBin whereSP :: Sing PrimeBin z data Sing PrimePower # data Sing PrimePower whereSPP :: Sing PrimePower z data Sing Factored # data Sing Factored whereSF :: Sing Factored z data Sing [a0] data Sing [a0] whereSNil :: Sing [a0] z0SCons :: Sing [a0] z0 data Sing (Maybe a0) data Sing (Maybe a0) whereSNothing :: Sing (Maybe a0) z0SJust :: Sing (Maybe a0) z0 data Sing (TyFun k1 k2 -> *) data Sing (TyFun k1 k2 -> *) = SLambda {applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)} data Sing (Either a0 b0) data Sing (Either a0 b0) whereSLeft :: Sing (Either a0 b0) z0SRight :: Sing (Either a0 b0) z0 data Sing (a0, b0) data Sing (a0, b0) whereSTuple2 :: Sing (a0, b0) z0 data Sing (a0, b0, c0) data Sing (a0, b0, c0) whereSTuple3 :: Sing (a0, b0, c0) z0 data Sing (a0, b0, c0, d0) data Sing (a0, b0, c0, d0) whereSTuple4 :: Sing (a0, b0, c0, d0) z0 data Sing (a0, b0, c0, d0, e0) data Sing (a0, b0, c0, d0, e0) whereSTuple5 :: Sing (a0, b0, c0, d0, e0) z0 data Sing (a0, b0, c0, d0, e0, f0) data Sing (a0, b0, c0, d0, e0, f0) whereSTuple6 :: 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) whereSTuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type SPos = (Sing :: Pos -> Type) Source #

type PosC p = SingI p Source #

Kind-restricted synonym for SingI.

posToInt :: C z => Pos -> z Source #

Convert a Pos to an integral type.

sAddPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AddPosSym0 t) t :: Pos) Source #

type family AddPos (a :: Pos) (a :: Pos) :: Pos where ... Source #

Equations

 AddPos O b = Apply SSym0 b AddPos (S a) b = Apply (Apply () SSym0) (Apply (Apply AddPosSym0 a) b)

sSubPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply SubPosSym0 t) t :: Pos) Source #

type family SubPos (a :: Pos) (a :: Pos) :: Pos where ... Source #

Equations

 SubPos (S a) O = a SubPos (S a) (S b) = Apply (Apply SubPosSym0 a) b SubPos O _z_1627476520 = Apply ErrorSym0 "Invalid call to subPos: a <= b"

reifyPos :: Int -> (forall p. SPos p -> a) -> a Source #

Reify a Pos as a singleton.

reifyPosI :: Int -> (forall p proxy. PosC p => proxy p -> a) -> a Source #

Reify a Pos for a SingI constraint.

Template Haskell splice for the Pos type representing a given Int, e.g., $(posType 8). Template Haskell splice that defines the Pos type synonym P$$n$$. type OSym0 = O Source # data SSym0 l Source # Instances  Source # MethodssuppressUnusedWarnings :: Proxy SSym0 t -> () # type Apply Pos Pos SSym0 l0 Source # type Apply Pos Pos SSym0 l0 = SSym1 l0 type SSym1 t = S t Source # data AddPosSym0 l Source # Instances  Source # Methods type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 Source # type Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 = AddPosSym1 l0 data AddPosSym1 l l Source # Instances  Source # Methods type Apply Pos Pos (AddPosSym1 l1) l0 Source # type Apply Pos Pos (AddPosSym1 l1) l0 data SubPosSym0 l Source # Instances  Source # Methods type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 Source # type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 = SubPosSym1 l0 data SubPosSym1 l l Source # Instances  Source # Methods type Apply Pos Pos (SubPosSym1 l1) l0 Source # type Apply Pos Pos (SubPosSym1 l1) l0 # Positive naturals in binary representation data Bin Source # Constructors  B1 D0 Bin D1 Bin Instances  Source # Methods(==) :: Bin -> Bin -> Bool #(/=) :: Bin -> Bin -> Bool # Source # Methodscompare :: Bin -> Bin -> Ordering #(<) :: Bin -> Bin -> Bool #(<=) :: Bin -> Bin -> Bool #(>) :: Bin -> Bin -> Bool #(>=) :: Bin -> Bin -> Bool #max :: Bin -> Bin -> Bin #min :: Bin -> Bin -> Bin # Source # MethodsshowsPrec :: Int -> Bin -> ShowS #show :: Bin -> String #showList :: [Bin] -> ShowS # Source # Methodssing :: Sing B1 a # Source # Associated Typestype Compare (KProxy Bin) (arg0 :: KProxy Bin) (arg1 :: KProxy Bin) :: Ordering #type ((KProxy Bin) :< (arg0 :: KProxy Bin)) (arg1 :: KProxy Bin) :: Bool #type ((KProxy Bin) :<= (arg0 :: KProxy Bin)) (arg1 :: KProxy Bin) :: Bool #type ((KProxy Bin) :> (arg0 :: KProxy Bin)) (arg1 :: KProxy Bin) :: Bool #type ((KProxy Bin) :>= (arg0 :: KProxy Bin)) (arg1 :: KProxy Bin) :: Bool #type Max (KProxy Bin) (arg0 :: KProxy Bin) (arg1 :: KProxy Bin) :: a0 #type Min (KProxy Bin) (arg0 :: KProxy Bin) (arg1 :: KProxy Bin) :: a0 # Source # MethodssCompare :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing Ordering (Apply (KProxy Bin) Ordering (Apply (KProxy Bin) (TyFun (KProxy Bin) Ordering -> Type) (CompareSym0 (KProxy Bin)) t0) t1) #(%:<) :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing Bool (Apply (KProxy Bin) Bool (Apply (KProxy Bin) (TyFun (KProxy Bin) Bool -> Type) ((:<$) (KProxy Bin)) t0) t1) #(%:<=) :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing Bool (Apply (KProxy Bin) Bool (Apply (KProxy Bin) (TyFun (KProxy Bin) Bool -> Type) ((:<=$) (KProxy Bin)) t0) t1) #(%:>) :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing Bool (Apply (KProxy Bin) Bool (Apply (KProxy Bin) (TyFun (KProxy Bin) Bool -> Type) ((:>$) (KProxy Bin)) t0) t1) #(%:>=) :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing Bool (Apply (KProxy Bin) Bool (Apply (KProxy Bin) (TyFun (KProxy Bin) Bool -> Type) ((:>=$) (KProxy Bin)) t0) t1) #sMax :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing (KProxy Bin) (Apply (KProxy Bin) (KProxy Bin) (Apply (KProxy Bin) (TyFun (KProxy Bin) (KProxy Bin) -> Type) (MaxSym0 (KProxy Bin)) t0) t1) #sMin :: Sing (KProxy Bin) t0 -> Sing (KProxy Bin) t1 -> Sing (KProxy Bin) (Apply (KProxy Bin) (KProxy Bin) (Apply (KProxy Bin) (TyFun (KProxy Bin) (KProxy Bin) -> Type) (MinSym0 (KProxy Bin)) t0) t1) # Source # Methods(%:==) :: Sing (KProxy Bin) a -> Sing (KProxy Bin) b -> Sing Bool ((KProxy Bin :== a) b) #(%:/=) :: Sing (KProxy Bin) a -> Sing (KProxy Bin) b -> Sing Bool ((KProxy Bin :/= a) b) # Source # Associated Typestype ((KProxy Bin) :== (x :: KProxy Bin)) (y :: KProxy Bin) :: Bool #type ((KProxy Bin) :/= (x :: KProxy Bin)) (y :: KProxy Bin) :: Bool # Source # Methods(%~) :: Sing (KProxy Bin) a -> Sing (KProxy Bin) b -> Decision ((KProxy Bin :~: a) b) # SingI Bin n0 => SingI Bin (D0 n0) Source # Methodssing :: Sing (D0 n0) a # SingI Bin n0 => SingI Bin (D1 n0) Source # Methodssing :: Sing (D1 n0) a # Source # Associated Typestype DemoteRep (KProxy Bin) (kparam :: KProxy (KProxy Bin)) :: * # MethodsfromSing :: Sing (KProxy Bin) a -> DemoteRep (KProxy Bin) kparam #toSing :: DemoteRep (KProxy Bin) kparam -> SomeSing (KProxy Bin) kparam # Source # MethodssuppressUnusedWarnings :: Proxy D1Sym0 t -> () # Source # MethodssuppressUnusedWarnings :: Proxy D0Sym0 t -> () # data Sing Bin Source # data Sing Bin whereSB1 :: Sing Bin zSD0 :: Sing Bin zSD1 :: Sing Bin z type Min Bin arg0 arg1 Source # type Min Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Min_1627682018Sym0 Bin) arg0) arg1 type Max Bin arg0 arg1 Source # type Max Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Max_1627681985Sym0 Bin) arg0) arg1 type (:>=) Bin arg0 arg1 Source # type (:>=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627681952Sym0 Bin) arg0) arg1 type (:>) Bin arg0 arg1 Source # type (:>) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627681919Sym0 Bin) arg0) arg1 type (:<=) Bin arg0 arg1 Source # type (:<=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627681886Sym0 Bin) arg0) arg1 type (:<) Bin arg0 arg1 Source # type (:<) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627681853Sym0 Bin) arg0) arg1 type Compare Bin a0 a1 Source # type Compare Bin a0 a1 type (:/=) Bin x y Source # type (:/=) Bin x y = Not ((:==) Bin x y) type (:==) Bin a0 b0 Source # type (:==) Bin a0 b0 type Apply Bin Bin D1Sym0 l0 Source # type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0 type Apply Bin Bin D0Sym0 l0 Source # type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0 type DemoteRep Bin (KProxy Bin) Source # type DemoteRep Bin (KProxy Bin) = Bin data family Sing k (a :: k) :: * # The singleton kind-indexed data family. Instances  data Sing Bool data Sing Bool whereSFalse :: Sing Bool z0STrue :: Sing Bool z0 data Sing Ordering data Sing Ordering whereSLT :: Sing Ordering z0SEQ :: Sing Ordering z0SGT :: Sing Ordering z0 data Sing Nat data Sing Nat whereSNat :: Sing Nat n data Sing Symbol data Sing Symbol whereSSym :: Sing Symbol n data Sing () data Sing () whereSTuple0 :: Sing () z0 data Sing Pos # data Sing Pos whereSO :: Sing Pos zSS :: Sing Pos z data Sing Bin # data Sing Bin whereSB1 :: Sing Bin zSD0 :: Sing Bin zSD1 :: Sing Bin z data Sing PrimeBin # data Sing PrimeBin whereSP :: Sing PrimeBin z data Sing PrimePower # data Sing PrimePower whereSPP :: Sing PrimePower z data Sing Factored # data Sing Factored whereSF :: Sing Factored z data Sing [a0] data Sing [a0] whereSNil :: Sing [a0] z0SCons :: Sing [a0] z0 data Sing (Maybe a0) data Sing (Maybe a0) whereSNothing :: Sing (Maybe a0) z0SJust :: Sing (Maybe a0) z0 data Sing (TyFun k1 k2 -> *) data Sing (TyFun k1 k2 -> *) = SLambda {applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)} data Sing (Either a0 b0) data Sing (Either a0 b0) whereSLeft :: Sing (Either a0 b0) z0SRight :: Sing (Either a0 b0) z0 data Sing (a0, b0) data Sing (a0, b0) whereSTuple2 :: Sing (a0, b0) z0 data Sing (a0, b0, c0) data Sing (a0, b0, c0) whereSTuple3 :: Sing (a0, b0, c0) z0 data Sing (a0, b0, c0, d0) data Sing (a0, b0, c0, d0) whereSTuple4 :: Sing (a0, b0, c0, d0) z0 data Sing (a0, b0, c0, d0, e0) data Sing (a0, b0, c0, d0, e0) whereSTuple5 :: Sing (a0, b0, c0, d0, e0) z0 data Sing (a0, b0, c0, d0, e0, f0) data Sing (a0, b0, c0, d0, e0, f0) whereSTuple6 :: 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) whereSTuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0 type SBin = (Sing :: Bin -> Type) Source # type BinC b = SingI b Source # Kind-restricted synonym for SingI. reifyBin :: Int -> (forall b. SBin b -> a) -> a Source # Reify a Bin as a singleton. reifyBinI :: Int -> (forall b proxy. BinC b => proxy b -> a) -> a Source # Reify a Bin for a SingI constraint. binToInt :: C z => Bin -> z Source # Convert a Bin to an integral type. Template Haskell splice for the Bin type representing a given Int, e.g., $(binType 89).

Template Haskell splice that defines the Bin type synonym B$$n$$.

type B1Sym0 = B1 Source #

data D0Sym0 l Source #

Instances

 Source # MethodssuppressUnusedWarnings :: Proxy D0Sym0 t -> () # type Apply Bin Bin D0Sym0 l0 Source # type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0

type D0Sym1 t = D0 t Source #

data D1Sym0 l Source #

Instances

 Source # MethodssuppressUnusedWarnings :: Proxy D1Sym0 t -> () # type Apply Bin Bin D1Sym0 l0 Source # type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0

type D1Sym1 t = D1 t Source #

# Miscellaneous

Arguments

 :: String pfx -> (Int -> TypeQ) f -> Int n -> DecQ

Template Haskell splice that declares a type synonym <pfx>$$n$$ as the type f n.

primes :: [Int] Source #

Infinite list of primes, built using Sieve of Erastothenes.

Search for the argument in primes. This is not particularly fast, but works well enough for moderate-sized numbers that would appear as (divisors of) cyclotomic indices of interest.

# Convenient synonyms for Pos and Bin types

type P1 = O Source #

type P2 = S O Source #

type P3 = S (S O) Source #

type P4 = S (S (S O)) Source #

type P5 = S (S (S (S O))) Source #

type P6 = S (S (S (S (S O)))) Source #

type P7 = S (S (S (S (S (S O))))) Source #

type P8 = S (S (S (S (S (S (S O)))))) Source #

type P9 = S (S (S (S (S (S (S (S O))))))) Source #

type P10 = S (S (S (S (S (S (S (S (S O)))))))) Source #

type P11 = S (S (S (S (S (S (S (S (S (S O))))))))) Source #

type P12 = S (S (S (S (S (S (S (S (S (S (S O)))))))))) Source #

type P13 = S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) Source #

type P14 = S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) Source #

type P15 = S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) Source #

type P16 = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))) Source #

type B1 = B1 Source #

type B2 = D0 B1 Source #

type B3 = D1 B1 Source #

type B4 = D0 (D0 B1) Source #

type B5 = D1 (D0 B1) Source #

type B6 = D0 (D1 B1) Source #

type B7 = D1 (D1 B1) Source #

type B8 = D0 (D0 (D0 B1)) Source #

type B9 = D1 (D0 (D0 B1)) Source #

type B10 = D0 (D1 (D0 B1)) Source #

type B11 = D1 (D1 (D0 B1)) Source #

type B12 = D0 (D0 (D1 B1)) Source #

type B13 = D1 (D0 (D1 B1)) Source #

type B14 = D0 (D1 (D1 B1)) Source #

type B15 = D1 (D1 (D1 B1)) Source #

type B16 = D0 (D0 (D0 (D0 B1))) Source #

type B17 = D1 (D0 (D0 (D0 B1))) Source #

type B18 = D0 (D1 (D0 (D0 B1))) Source #

type B19 = D1 (D1 (D0 (D0 B1))) Source #

type B20 = D0 (D0 (D1 (D0 B1))) Source #

type B21 = D1 (D0 (D1 (D0 B1))) Source #

type B22 = D0 (D1 (D1 (D0 B1))) Source #

type B23 = D1 (D1 (D1 (D0 B1))) Source #

type B24 = D0 (D0 (D0 (D1 B1))) Source #

type B25 = D1 (D0 (D0 (D1 B1))) Source #

type B26 = D0 (D1 (D0 (D1 B1))) Source #

type B27 = D1 (D1 (D0 (D1 B1))) Source #

type B28 = D0 (D0 (D1 (D1 B1))) Source #

type B29 = D1 (D0 (D1 (D1 B1))) Source #

type B30 = D0 (D1 (D1 (D1 B1))) Source #

type B31 = D1 (D1 (D1 (D1 B1))) Source #

type B32 = D0 (D0 (D0 (D0 (D0 B1)))) Source #

type B33 = D1 (D0 (D0 (D0 (D0 B1)))) Source #

type B34 = D0 (D1 (D0 (D0 (D0 B1)))) Source #

type B35 = D1 (D1 (D0 (D0 (D0 B1)))) Source #

type B36 = D0 (D0 (D1 (D0 (D0 B1)))) Source #

type B37 = D1 (D0 (D1 (D0 (D0 B1)))) Source #

type B38 = D0 (D1 (D1 (D0 (D0 B1)))) Source #

type B39 = D1 (D1 (D1 (D0 (D0 B1)))) Source #

type B40 = D0 (D0 (D0 (D1 (D0 B1)))) Source #

type B41 = D1 (D0 (D0 (D1 (D0 B1)))) Source #

type B42 = D0 (D1 (D0 (D1 (D0 B1)))) Source #

type B43 = D1 (D1 (D0 (D1 (D0 B1)))) Source #

type B44 = D0 (D0 (D1 (D1 (D0 B1)))) Source #

type B45 = D1 (D0 (D1 (D1 (D0 B1)))) Source #

type B46 = D0 (D1 (D1 (D1 (D0 B1)))) Source #

type B47 = D1 (D1 (D1 (D1 (D0 B1)))) Source #

type B48 = D0 (D0 (D0 (D0 (D1 B1)))) Source #

type B49 = D1 (D0 (D0 (D0 (D1 B1)))) Source #

type B50 = D0 (D1 (D0 (D0 (D1 B1)))) Source #

type B51 = D1 (D1 (D0 (D0 (D1 B1)))) Source #

type B52 = D0 (D0 (D1 (D0 (D1 B1)))) Source #

type B53 = D1 (D0 (D1 (D0 (D1 B1)))) Source #

type B54 = D0 (D1 (D1 (D0 (D1 B1)))) Source #

type B55 = D1 (D1 (D1 (D0 (D1 B1)))) Source #

type B56 = D0 (D0 (D0 (D1 (D1 B1)))) Source #

type B57 = D1 (D0 (D0 (D1 (D1 B1)))) Source #

type B58 = D0 (D1 (D0 (D1 (D1 B1)))) Source #

type B59 = D1 (D1 (D0 (D1 (D1 B1)))) Source #

type B60 = D0 (D0 (D1 (D1 (D1 B1)))) Source #

type B61 = D1 (D0 (D1 (D1 (D1 B1)))) Source #

type B62 = D0 (D1 (D1 (D1 (D1 B1)))) Source #

type B63 = D1 (D1 (D1 (D1 (D1 B1)))) Source #

type B64 = D0 (D0 (D0 (D0 (D0 (D0 B1))))) Source #

type B65 = D1 (D0 (D0 (D0 (D0 (D0 B1))))) Source #

type B66 = D0 (D1 (D0 (D0 (D0 (D0 B1))))) Source #

type B67 = D1 (D1 (D0 (D0 (D0 (D0 B1))))) Source #

type B68 = D0 (D0 (D1 (D0 (D0 (D0 B1))))) Source #

type B69 = D1 (D0 (D1 (D0 (D0 (D0 B1))))) Source #

type B70 = D0 (D1 (D1 (D0 (D0 (D0 B1))))) Source #

type B71 = D1 (D1 (D1 (D0 (D0 (D0 B1))))) Source #

type B72 = D0 (D0 (D0 (D1 (D0 (D0 B1))))) Source #

type B73 = D1 (D0 (D0 (D1 (D0 (D0 B1))))) Source #

type B74 = D0 (D1 (D0 (D1 (D0 (D0 B1))))) Source #

type B75 = D1 (D1 (D0 (D1 (D0 (D0 B1))))) Source #

type B76 = D0 (D0 (D1 (D1 (D0 (D0 B1))))) Source #

type B77 = D1 (D0 (D1 (D1 (D0 (D0 B1))))) Source #

type B78 = D0 (D1 (D1 (D1 (D0 (D0 B1))))) Source #

type B79 = D1 (D1 (D1 (D1 (D0 (D0 B1))))) Source #

type B80 = D0 (D0 (D0 (D0 (D1 (D0 B1))))) Source #

type B81 = D1 (D0 (D0 (D0 (D1 (D0 B1))))) Source #

type B82 = D0 (D1 (D0 (D0 (D1 (D0 B1))))) Source #

type B83 = D1 (D1 (D0 (D0 (D1 (D0 B1))))) Source #

type B84 = D0 (D0 (D1 (D0 (D1 (D0 B1))))) Source #

type B85 = D1 (D0 (D1 (D0 (D1 (D0 B1))))) Source #

type B86 = D0 (D1 (D1 (D0 (D1 (D0 B1))))) Source #

type B87 = D1 (D1 (D1 (D0 (D1 (D0 B1))))) Source #

type B88 = D0 (D0 (D0 (D1 (D1 (D0 B1))))) Source #

type B89 = D1 (D0 (D0 (D1 (D1 (D0 B1))))) Source #

type B90 = D0 (D1 (D0 (D1 (D1 (D0 B1))))) Source #

type B91 = D1 (D1 (D0 (D1 (D1 (D0 B1))))) Source #

type B92 = D0 (D0 (D1 (D1 (D1 (D0 B1))))) Source #

type B93 = D1 (D0 (D1 (D1 (D1 (D0 B1))))) Source #

type B94 = D0 (D1 (D1 (D1 (D1 (D0 B1))))) Source #

type B95 = D1 (D1 (D1 (D1 (D1 (D0 B1))))) Source #

type B96 = D0 (D0 (D0 (D0 (D0 (D1 B1))))) Source #

type B97 = D1 (D0 (D0 (D0 (D0 (D1 B1))))) Source #

type B98 = D0 (D1 (D0 (D0 (D0 (D1 B1))))) Source #

type B99 = D1 (D1 (D0 (D0 (D0 (D1 B1))))) Source #

type B100 = D0 (D0 (D1 (D0 (D0 (D1 B1))))) Source #

type B101 = D1 (D0 (D1 (D0 (D0 (D1 B1))))) Source #

type B102 = D0 (D1 (D1 (D0 (D0 (D1 B1))))) Source #

type B103 = D1 (D1 (D1 (D0 (D0 (D1 B1))))) Source #

type B104 = D0 (D0 (D0 (D1 (D0 (D1 B1))))) Source #

type B105 = D1 (D0 (D0 (D1 (D0 (D1 B1))))) Source #

type B106 = D0 (D1 (D0 (D1 (D0 (D1 B1))))) Source #

type B107 = D1 (D1 (D0 (D1 (D0 (D1 B1))))) Source #

type B108 = D0 (D0 (D1 (D1 (D0 (D1 B1))))) Source #

type B109 = D1 (D0 (D1 (D1 (D0 (D1 B1))))) Source #

type B110 = D0 (D1 (D1 (D1 (D0 (D1 B1))))) Source #

type B111 = D1 (D1 (D1 (D1 (D0 (D1 B1))))) Source #

type B112 = D0 (D0 (D0 (D0 (D1 (D1 B1))))) Source #

type B113 = D1 (D0 (D0 (D0 (D1 (D1 B1))))) Source #

type B114 = D0 (D1 (D0 (D0 (D1 (D1 B1))))) Source #

type B115 = D1 (D1 (D0 (D0 (D1 (D1 B1))))) Source #

type B116 = D0 (D0 (D1 (D0 (D1 (D1 B1))))) Source #

type B117 = D1 (D0 (D1 (D0 (D1 (D1 B1))))) Source #

type B118 = D0 (D1 (D1 (D0 (D1 (D1 B1))))) Source #

type B119 = D1 (D1 (D1 (D0 (D1 (D1 B1))))) Source #

type B120 = D0 (D0 (D0 (D1 (D1 (D1 B1))))) Source #

type B121 = D1 (D0 (D0 (D1 (D1 (D1 B1))))) Source #

type B122 = D0 (D1 (D0 (D1 (D1 (D1 B1))))) Source #

type B123 = D1 (D1 (D0 (D1 (D1 (D1 B1))))) Source #

type B124 = D0 (D0 (D1 (D1 (D1 (D1 B1))))) Source #

type B125 = D1 (D0 (D1 (D1 (D1 (D1 B1))))) Source #

type B126 = D0 (D1 (D1 (D1 (D1 (D1 B1))))) Source #

type B127 = D1 (D1 (D1 (D1 (D1 (D1 B1))))) Source #

type B128 = D0 (D0 (D0 (D0 (D0 (D0 (D0 B1)))))) Source #

# Convenient synonyms for Factored, PrimePower, and Prime types

type F1 = F '[] Source #

type F2 = F '[PP '(P (D0 B1), O)] Source #

type F3 = F '[PP '(P (D1 B1), O)] Source #

type F4 = F '[PP '(P (D0 B1), S O)] Source #

type F5 = F '[PP '(P (D1 (D0 B1)), O)] Source #

type F6 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O)] Source #

type F7 = F '[PP '(P (D1 (D1 B1)), O)] Source #

type F8 = F '[PP '(P (D0 B1), S (S O))] Source #

type F9 = F '[PP '(P (D1 B1), S O)] Source #

type F10 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O)] Source #

type F11 = F '[PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F12 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O)] Source #

type F13 = F '[PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F14 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O)] Source #

type F15 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)] Source #

type F16 = F '[PP '(P (D0 B1), S (S (S O)))] Source #

type F17 = F '[PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F18 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O)] Source #

type F19 = F '[PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F20 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O)] Source #

type F21 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)] Source #

type F22 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F23 = F '[PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F24 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O)] Source #

type F25 = F '[PP '(P (D1 (D0 B1)), S O)] Source #

type F26 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F27 = F '[PP '(P (D1 B1), S (S O))] Source #

type F28 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), O)] Source #

type F29 = F '[PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F30 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)] Source #

type F31 = F '[PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F32 = F '[PP '(P (D0 B1), S (S (S (S O))))] Source #

type F33 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F34 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F35 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)] Source #

type F36 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O)] Source #

type F37 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F38 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F39 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F40 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), O)] Source #

type F41 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

type F42 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)] Source #

type F43 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

type F44 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F45 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)] Source #

type F46 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F47 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)] Source #

type F48 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), O)] Source #

type F49 = F '[PP '(P (D1 (D1 B1)), S O)] Source #

type F50 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), S O)] Source #

type F51 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F52 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F53 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)] Source #

type F54 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S O))] Source #

type F55 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F56 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 B1)), O)] Source #

type F57 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F58 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F59 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)] Source #

type F60 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)] Source #

type F61 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)] Source #

type F62 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F63 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)] Source #

type F64 = F '[PP '(P (D0 B1), S (S (S (S (S O)))))] Source #

type F65 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F66 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F67 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)] Source #

type F68 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F69 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F70 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)] Source #

type F71 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)] Source #

type F72 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S O)] Source #

type F73 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)] Source #

type F74 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F75 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S O)] Source #

type F76 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F77 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F78 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F79 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)] Source #

type F80 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 B1)), O)] Source #

type F81 = F '[PP '(P (D1 B1), S (S (S O)))] Source #

type F82 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

type F83 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)] Source #

type F84 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)] Source #

type F85 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F86 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

type F87 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F88 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F89 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)] Source #

type F90 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)] Source #

type F91 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F92 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F93 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F94 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)] Source #

type F95 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F96 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 B1), O)] Source #

type F97 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)] Source #

type F98 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), S O)] Source #

type F99 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F100 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), S O)] Source #

type F101 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)] Source #

type F102 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F103 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)] Source #

type F104 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F105 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)] Source #

type F106 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)] Source #

type F107 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)] Source #

type F108 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S (S O))] Source #

type F109 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)] Source #

type F110 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F111 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F112 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 B1)), O)] Source #

type F113 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)] Source #

type F114 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F115 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F116 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F117 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F118 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)] Source #

type F119 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F120 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O)] Source #

type F121 = F '[PP '(P (D1 (D1 (D0 B1))), S O)] Source #

type F122 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)] Source #

type F123 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

type F124 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F125 = F '[PP '(P (D1 (D0 B1)), S (S O))] Source #

type F126 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 B1)), O)] Source #

type F127 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))), O)] Source #

type F128 = F '[PP '(P (D0 B1), S (S (S (S (S (S O))))))] Source #

type F129 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

type F130 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F131 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))), O)] Source #

type F132 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F133 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F134 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)] Source #

type F135 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D0 B1)), O)] Source #

type F136 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F137 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)] Source #

type F138 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F139 = F '[PP '(P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))), O)] Source #

type F140 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)] Source #

type F141 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)] Source #

type F142 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)] Source #

type F143 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F144 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 B1), S O)] Source #

type F145 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F146 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)] Source #

type F147 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), S O)] Source #

type F148 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F149 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)] Source #

type F150 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), S O)] Source #

type F151 = F '[PP '(P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))), O)] Source #

type F152 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F153 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F154 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F155 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F156 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F157 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))), O)] Source #

type F158 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))), O)] Source #

type F159 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)] Source #

type F160 = F '[PP '(P (D0 B1), S (S (S (S O)))), PP '(P (D1 (D0 B1)), O)] Source #

type F161 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F162 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S (S (S O)))] Source #

type F163 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)] Source #

type F164 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

type F165 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F166 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)] Source #

type F167 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))), O)] Source #

type F168 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), O), PP '(P (D1 (D1 B1)), O)] Source #

type F169 = F '[PP '(P (D1 (D0 (D1 B1))), S O)] Source #

type F170 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F171 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F172 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

type F173 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))), O)] Source #

type F174 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F175 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 B1)), O)] Source #

type F176 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F177 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)] Source #

type F178 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)] Source #

type F179 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))), O)] Source #

type F180 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), S O), PP '(P (D1 (D0 B1)), O)] Source #

type F181 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1))))))), O)] Source #

type F182 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F183 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)] Source #

type F184 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F185 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F186 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F187 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F188 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D1 (D0 B1))))), O)] Source #

type F189 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D1 B1)), O)] Source #

type F190 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F191 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))), O)] Source #

type F192 = F '[PP '(P (D0 B1), S (S (S (S (S O))))), PP '(P (D1 B1), O)] Source #

type F193 = F '[PP '(P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))), O)] Source #

type F194 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)] Source #

type F195 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F196 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), S O)] Source #

type F197 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))), O)] Source #

type F198 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F199 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))), O)] Source #

type F200 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 B1)), S O)] Source #

type F201 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))), O)] Source #

type F202 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)] Source #

type F203 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F204 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F205 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

type F206 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))), O)] Source #

type F207 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F208 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F209 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

type F210 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 B1)), O)] Source #

type F211 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))), O)] Source #

type F212 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)] Source #

type F213 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))), O)] Source #

type F214 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))), O)] Source #

type F215 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

type F216 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 B1), S (S O))] Source #

type F217 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D1 (D1 B1)))), O)] Source #

type F218 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)] Source #

type F219 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)] Source #

type F220 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F221 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F222 = F '[PP '(P (D0 B1), O), PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

type F223 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))), O)] Source #

type F224 = F '[PP '(P (D0 B1), S (