lol-0.4.0.0: A library for lattice cryptography.

Safe HaskellNone
LanguageHaskell2010

Crypto.Lol.Factored

Contents

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

Eq Factored Source # 
Show Factored Source # 
(Fact m, C i) => Reflects Factored m i Source # 

Methods

value :: Tagged m i i Source #

SEq Factored (KProxy Factored) Source # 
PEq Factored (KProxy Factored) Source # 

Associated Types

type ((KProxy Factored) :== (x :: KProxy Factored)) (y :: KProxy Factored) :: Bool #

type ((KProxy Factored) :/= (x :: KProxy Factored)) (y :: KProxy Factored) :: Bool #

SDecide Factored (KProxy Factored) Source # 
SingKind Factored (KProxy Factored) Source # 

Associated Types

type DemoteRep (KProxy Factored) (kparam :: KProxy (KProxy Factored)) :: * #

data Sing Factored Source # 
data Sing Factored where
type (:/=) Factored x y Source # 
type (:/=) Factored x y = Not ((:==) Factored x y)
type (:==) Factored a0 b0 Source # 
type (:==) Factored a0 b0
type DemoteRep Factored (KProxy Factored) Source # 

type Fact m = SingI m Source #

Kind-restricted synonym for SingI.

fType :: Int -> TypeQ Source #

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).

fDec :: Int -> DecQ Source #

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.

data PrimePower Source #

Instances

Eq PrimePower Source # 
Show PrimePower Source # 
(PPow pp, C i) => Reflects PrimePower pp i Source # 

Methods

value :: Tagged pp i i Source #

SEq PrimePower (KProxy PrimePower) Source # 
PEq PrimePower (KProxy PrimePower) Source # 

Associated Types

type ((KProxy PrimePower) :== (x :: KProxy PrimePower)) (y :: KProxy PrimePower) :: Bool #

type ((KProxy PrimePower) :/= (x :: KProxy PrimePower)) (y :: KProxy PrimePower) :: Bool #

SDecide PrimePower (KProxy PrimePower) Source # 
SingKind PrimePower (KProxy PrimePower) Source # 

Associated Types

type DemoteRep (KProxy PrimePower) (kparam :: KProxy (KProxy PrimePower)) :: * #

(PPow pp, (~) * zq (ZqBasic PrimePower pp z), PrimeField (ZpOf zq), Ring zq) => ZPP (ZqBasic PrimePower pp z) Source # 

Associated Types

type ZpOf (ZqBasic PrimePower pp z) :: * Source #

data Sing PrimePower Source # 
type (:/=) PrimePower x y Source # 
type (:==) PrimePower a0 b0 Source # 
type (:==) PrimePower a0 b0
type DemoteRep PrimePower (KProxy PrimePower) Source # 
type ZpOf (ZqBasic PrimePower pp z) Source # 

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

The singleton kind-indexed data family.

Instances

data Sing Bool 
data Sing Bool where
data Sing Ordering 
data Sing Nat 
data Sing Nat where
data Sing Symbol 
data Sing Symbol where
data Sing () 
data Sing () where
data Sing Pos # 
data Sing Pos where
data Sing Bin # 
data Sing Bin where
data Sing PrimeBin # 
data Sing PrimeBin where
data Sing PrimePower # 
data Sing Factored # 
data Sing Factored where
data Sing [a0] 
data Sing [a0] where
data Sing (Maybe a0) 
data Sing (Maybe a0) where
data Sing (TyFun k1 k2 -> *) 
data Sing (TyFun k1 k2 -> *) = SLambda {}
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing (a0, b0, c0) 
data Sing (a0, b0, c0) where
data Sing (a0, b0, c0, d0) 
data Sing (a0, b0, c0, d0) where
data Sing (a0, b0, c0, d0, e0) 
data Sing (a0, b0, c0, d0, e0) where
data Sing (a0, b0, c0, d0, e0, f0) 
data Sing (a0, b0, c0, d0, e0, f0) where
data Sing (a0, b0, c0, d0, e0, f0, g0) 
data Sing (a0, b0, c0, d0, e0, f0, g0) where

type PPow pp = SingI pp Source #

Kind-restricted synonym for SingI.

ppType :: PP -> TypeQ Source #

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.

ppDec :: PP -> DecQ Source #

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

Eq PrimeBin Source # 
Ord PrimeBin Source # 
Show PrimeBin Source # 
(Prime p, C i) => Reflects PrimeBin p i Source # 

Methods

value :: Tagged p i i Source #

POrd PrimeBin (KProxy PrimeBin) Source # 

Associated Types

type 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 #

SOrd Bin (KProxy Bin) => SOrd PrimeBin (KProxy PrimeBin) Source # 

Methods

sCompare :: 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) #

SEq PrimeBin (KProxy PrimeBin) Source # 
PEq PrimeBin (KProxy PrimeBin) Source # 

Associated Types

type ((KProxy PrimeBin) :== (x :: KProxy PrimeBin)) (y :: KProxy PrimeBin) :: Bool #

type ((KProxy PrimeBin) :/= (x :: KProxy PrimeBin)) (y :: KProxy PrimeBin) :: Bool #

SDecide PrimeBin (KProxy PrimeBin) Source # 
SingKind PrimeBin (KProxy PrimeBin) Source # 

Associated Types

type DemoteRep (KProxy PrimeBin) (kparam :: KProxy (KProxy PrimeBin)) :: * #

data Sing PrimeBin Source # 
data Sing PrimeBin where
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
type DemoteRep PrimeBin (KProxy PrimeBin) Source # 

type Prime p = SingI p Source #

Kind-restricted synonym for SingI.

pType :: Int -> TypeQ Source #

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).

pDec :: Int -> DecQ Source #

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

FOddRadical (F pps) = Apply FSym0 (Apply PpsOddRadSym0 pps) 

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.

valueFact :: Fact m => Tagged m Int Source #

The value of a Factored type.

totientFact :: Fact m => Tagged m Int Source #

The totient of a Factored type's value.

valueHatFact :: Fact m => Tagged m Int Source #

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} \).

radicalFact :: Fact m => Tagged m Int Source #

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

oddRadicalFact :: Fact m => Tagged m Int Source #

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.

ppToPP :: PrimePower -> PP Source #

Conversion.

valuePP :: PP -> Int Source #

The value of a prime power.

totientPP :: PP -> Int Source #

Totient of a prime power.

radicalPP :: PP -> Int Source #

The radical of a prime power.

oddRadicalPP :: PP -> Int Source #

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

Re-export

Positive naturals in Peano representation

data Pos Source #

Constructors

O 
S Pos 

Instances

Eq Pos Source # 

Methods

(==) :: Pos -> Pos -> Bool #

(/=) :: Pos -> Pos -> Bool #

Ord Pos Source # 

Methods

compare :: Pos -> Pos -> Ordering #

(<) :: Pos -> Pos -> Bool #

(<=) :: Pos -> Pos -> Bool #

(>) :: Pos -> Pos -> Bool #

(>=) :: Pos -> Pos -> Bool #

max :: Pos -> Pos -> Pos #

min :: Pos -> Pos -> Pos #

Show Pos Source # 

Methods

showsPrec :: Int -> Pos -> ShowS #

show :: Pos -> String #

showList :: [Pos] -> ShowS #

SingI Pos O Source # 

Methods

sing :: Sing O a #

POrd Pos (KProxy Pos) Source # 

Associated Types

type 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 #

SOrd Pos (KProxy Pos) Source # 
SEq Pos (KProxy Pos) 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) #

PEq Pos (KProxy Pos) Source # 

Associated Types

type ((KProxy Pos) :== (x :: KProxy Pos)) (y :: KProxy Pos) :: Bool #

type ((KProxy Pos) :/= (x :: KProxy Pos)) (y :: KProxy Pos) :: Bool #

SDecide Pos (KProxy Pos) Source # 

Methods

(%~) :: Sing (KProxy Pos) a -> Sing (KProxy Pos) b -> Decision ((KProxy Pos :~: a) b) #

SingI Pos n0 => SingI Pos (S n0) Source # 

Methods

sing :: Sing (S n0) a #

SingKind Pos (KProxy Pos) Source # 

Associated Types

type DemoteRep (KProxy Pos) (kparam :: KProxy (KProxy Pos)) :: * #

Methods

fromSing :: Sing (KProxy Pos) a -> DemoteRep (KProxy Pos) kparam #

toSing :: DemoteRep (KProxy Pos) kparam -> SomeSing (KProxy Pos) kparam #

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) AddPosSym1 Source # 
SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) SubPosSym1 Source # 
SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) AddPosSym0 Source # 
SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> Type) -> *) SubPosSym0 Source # 
SuppressUnusedWarnings (TyFun Pos Pos -> *) SSym0 Source # 
data Sing Pos Source # 
data Sing Pos where
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 Apply Pos (TyFun Pos Pos -> Type) AddPosSym0 l0 Source # 
type Apply Pos (TyFun Pos Pos -> Type) SubPosSym0 l0 Source # 

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

The singleton kind-indexed data family.

Instances

data Sing Bool 
data Sing Bool where
data Sing Ordering 
data Sing Nat 
data Sing Nat where
data Sing Symbol 
data Sing Symbol where
data Sing () 
data Sing () where
data Sing Pos # 
data Sing Pos where
data Sing Bin # 
data Sing Bin where
data Sing PrimeBin # 
data Sing PrimeBin where
data Sing PrimePower # 
data Sing Factored # 
data Sing Factored where
data Sing [a0] 
data Sing [a0] where
data Sing (Maybe a0) 
data Sing (Maybe a0) where
data Sing (TyFun k1 k2 -> *) 
data Sing (TyFun k1 k2 -> *) = SLambda {}
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing (a0, b0, c0) 
data Sing (a0, b0, c0) where
data Sing (a0, b0, c0, d0) 
data Sing (a0, b0, c0, d0) where
data Sing (a0, b0, c0, d0, e0) 
data Sing (a0, b0, c0, d0, e0) where
data Sing (a0, b0, c0, d0, e0, f0) 
data Sing (a0, b0, c0, d0, e0, f0) where
data Sing (a0, b0, c0, d0, e0, f0, g0) 
data Sing (a0, b0, c0, d0, e0, f0, g0) where

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.

posType :: Int -> TypeQ Source #

Template Haskell splice for the Pos type representing a given Int, e.g., $(posType 8).

posDec :: Int -> DecQ Source #

Template Haskell splice that defines the Pos type synonym P\(n\).

type OSym0 = O Source #

type SSym1 t = S t Source #

Positive naturals in binary representation

data Bin Source #

Constructors

B1 
D0 Bin 
D1 Bin 

Instances

Eq Bin Source # 

Methods

(==) :: Bin -> Bin -> Bool #

(/=) :: Bin -> Bin -> Bool #

Ord Bin Source # 

Methods

compare :: Bin -> Bin -> Ordering #

(<) :: Bin -> Bin -> Bool #

(<=) :: Bin -> Bin -> Bool #

(>) :: Bin -> Bin -> Bool #

(>=) :: Bin -> Bin -> Bool #

max :: Bin -> Bin -> Bin #

min :: Bin -> Bin -> Bin #

Show Bin Source # 

Methods

showsPrec :: Int -> Bin -> ShowS #

show :: Bin -> String #

showList :: [Bin] -> ShowS #

SingI Bin B1 Source # 

Methods

sing :: Sing B1 a #

POrd Bin (KProxy Bin) Source # 

Associated Types

type 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 #

SOrd Bin (KProxy Bin) Source # 
SEq Bin (KProxy Bin) 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) #

PEq Bin (KProxy Bin) Source # 

Associated Types

type ((KProxy Bin) :== (x :: KProxy Bin)) (y :: KProxy Bin) :: Bool #

type ((KProxy Bin) :/= (x :: KProxy Bin)) (y :: KProxy Bin) :: Bool #

SDecide Bin (KProxy Bin) Source # 

Methods

(%~) :: Sing (KProxy Bin) a -> Sing (KProxy Bin) b -> Decision ((KProxy Bin :~: a) b) #

SingI Bin n0 => SingI Bin (D0 n0) Source # 

Methods

sing :: Sing (D0 n0) a #

SingI Bin n0 => SingI Bin (D1 n0) Source # 

Methods

sing :: Sing (D1 n0) a #

SingKind Bin (KProxy Bin) Source # 

Associated Types

type DemoteRep (KProxy Bin) (kparam :: KProxy (KProxy Bin)) :: * #

Methods

fromSing :: Sing (KProxy Bin) a -> DemoteRep (KProxy Bin) kparam #

toSing :: DemoteRep (KProxy Bin) kparam -> SomeSing (KProxy Bin) kparam #

SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0 Source # 
SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0 Source # 
data Sing Bin Source # 
data Sing Bin where
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 # 

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

The singleton kind-indexed data family.

Instances

data Sing Bool 
data Sing Bool where
data Sing Ordering 
data Sing Nat 
data Sing Nat where
data Sing Symbol 
data Sing Symbol where
data Sing () 
data Sing () where
data Sing Pos # 
data Sing Pos where
data Sing Bin # 
data Sing Bin where
data Sing PrimeBin # 
data Sing PrimeBin where
data Sing PrimePower # 
data Sing Factored # 
data Sing Factored where
data Sing [a0] 
data Sing [a0] where
data Sing (Maybe a0) 
data Sing (Maybe a0) where
data Sing (TyFun k1 k2 -> *) 
data Sing (TyFun k1 k2 -> *) = SLambda {}
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing (a0, b0, c0) 
data Sing (a0, b0, c0) where
data Sing (a0, b0, c0, d0) 
data Sing (a0, b0, c0, d0) where
data Sing (a0, b0, c0, d0, e0) 
data Sing (a0, b0, c0, d0, e0) where
data Sing (a0, b0, c0, d0, e0, f0) 
data Sing (a0, b0, c0, d0, e0, f0) where
data Sing (a0, b0, c0, d0, e0, f0, g0) 
data Sing (a0, b0, c0, d0, e0, f0, g0) where

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.

binType :: Int -> TypeQ Source #

Template Haskell splice for the Bin type representing a given Int, e.g., $(binType 89).

binDec :: Int -> DecQ Source #

Template Haskell splice that defines the Bin type synonym B\(n\).

type B1Sym0 = B1 Source #

type D0Sym1 t = D0 t Source #

type D1Sym1 t = D1 t Source #

Miscellaneous

intDec Source #

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.

prime :: Int -> Bool Source #

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 (