lol-0.6.0.0: A library for lattice cryptography.

Copyright(c) Eric Crockett 2011-2017
Chris Peikert 2011-2017
LicenseGPL-2
Maintainerecrockett0@email.com
Stabilityexperimental
PortabilityPOSIX \( \def\lcm{\text{lcm}} \)
Safe HaskellNone
LanguageHaskell2010

Crypto.Lol.Factored

Contents

Description

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

data Factored Source #

Instances

Eq Factored Source # 
Show Factored Source # 
SEq Factored Source # 

Methods

(%:==) :: Sing Factored a -> Sing Factored b -> Sing Bool ((Factored :== a) b) #

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

SDecide Factored Source # 

Methods

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

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

Methods

value :: Tagged m i i Source #

PEq Factored (Proxy * Factored) Source # 

Associated Types

type ((Proxy * Factored) :== (x :: Proxy * Factored)) (y :: Proxy * Factored) :: Bool #

type ((Proxy * Factored) :/= (x :: Proxy * Factored)) (y :: Proxy * Factored) :: Bool #

Fact m => Show (ArgType Factored m) # 
data Sing Factored Source # 
data Sing Factored where
type DemoteRep Factored Source # 
type (:/=) Factored x y Source # 
type (:/=) Factored x y = Not ((:==) Factored x y)
type (:==) Factored a0 b0 Source # 
type (:==) Factored a0 b0

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

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.

intToFact :: Int -> Factored Source #

Converts input to its data-level Factored representation.

Prime powers

data PrimePower Source #

Instances

Eq PrimePower Source # 
Show PrimePower Source # 
SEq PrimePower Source # 
SDecide PrimePower Source # 

Methods

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

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

Methods

value :: Tagged pp i i Source #

PEq PrimePower (Proxy * PrimePower) Source # 

Associated Types

type ((Proxy * PrimePower) :== (x :: Proxy * PrimePower)) (y :: Proxy * PrimePower) :: Bool #

type ((Proxy * PrimePower) :/= (x :: Proxy * PrimePower)) (y :: Proxy * PrimePower) :: Bool #

(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 DemoteRep PrimePower Source # 
type (:/=) PrimePower x y Source # 
type (:==) PrimePower a0 b0 Source # 
type (:==) PrimePower a0 b0
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 (NonEmpty a0) 
data Sing (NonEmpty a0) where
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing ((~>) k1 k2) 
data Sing ((~>) k1 k2) = SLambda {}
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 \).

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.

Primes

data PrimeBin Source #

Instances

Eq PrimeBin Source # 
Ord PrimeBin Source # 
Show PrimeBin Source # 
SOrd Bin => SOrd PrimeBin Source # 
SEq PrimeBin Source # 

Methods

(%:==) :: Sing PrimeBin a -> Sing PrimeBin b -> Sing Bool ((PrimeBin :== a) b) #

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

SDecide PrimeBin Source # 

Methods

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

SingKind PrimeBin Source # 
(Prime p, C i) => Reflects PrimeBin p i Source # 

Methods

value :: Tagged p i i Source #

POrd PrimeBin (Proxy * PrimeBin) Source # 

Associated Types

type Compare (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: Ordering #

type ((Proxy * PrimeBin) :< (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool #

type ((Proxy * PrimeBin) :<= (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool #

type ((Proxy * PrimeBin) :> (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool #

type ((Proxy * PrimeBin) :>= (arg0 :: Proxy * PrimeBin)) (arg1 :: Proxy * PrimeBin) :: Bool #

type Max (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: a0 #

type Min (Proxy * PrimeBin) (arg0 :: Proxy * PrimeBin) (arg1 :: Proxy * PrimeBin) :: a0 #

PEq PrimeBin (Proxy * PrimeBin) Source # 

Associated Types

type ((Proxy * PrimeBin) :== (x :: Proxy * PrimeBin)) (y :: Proxy * PrimeBin) :: Bool #

type ((Proxy * PrimeBin) :/= (x :: Proxy * PrimeBin)) (y :: Proxy * PrimeBin) :: Bool #

data Sing PrimeBin Source # 
data Sing PrimeBin where
type DemoteRep PrimeBin Source # 
type Min PrimeBin arg0 arg1 Source # 
type Min PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Min_1627688153Sym0 PrimeBin) arg0) arg1
type Max PrimeBin arg0 arg1 Source # 
type Max PrimeBin arg0 arg1 = Apply PrimeBin PrimeBin (Apply PrimeBin (TyFun PrimeBin PrimeBin -> Type) (Max_1627688120Sym0 PrimeBin) arg0) arg1
type (:>=) PrimeBin arg0 arg1 Source # 
type (:>=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688087Sym0 PrimeBin) arg0) arg1
type (:>) PrimeBin arg0 arg1 Source # 
type (:>) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688054Sym0 PrimeBin) arg0) arg1
type (:<=) PrimeBin arg0 arg1 Source # 
type (:<=) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627688021Sym0 PrimeBin) arg0) arg1
type (:<) PrimeBin arg0 arg1 Source # 
type (:<) PrimeBin arg0 arg1 = Apply PrimeBin Bool (Apply PrimeBin (TyFun PrimeBin Bool -> Type) (TFHelper_1627687988Sym0 PrimeBin) arg0) arg1
type Compare PrimeBin a1 a0 Source # 
type Compare PrimeBin a1 a0
type (:/=) PrimeBin x y Source # 
type (:/=) PrimeBin x y = Not ((:==) PrimeBin x y)
type (:==) PrimeBin a0 b0 Source # 
type (:==) PrimeBin a0 b0

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

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.

valueP :: PrimeBin -> Int Source #

Value of a PrimeBin.

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_1627689243 = Apply (Apply (Apply (:.$) PpToFSym0) PToPPSym0) a_1627689243 

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_1627678502 = Apply (Apply (Apply (:.$) FstSym0) UnPPSym0) a_1627678502 

type family ExponentPP (a :: PrimePower) :: Pos where ... Source #

Equations

ExponentPP a_1627678509 = Apply (Apply (Apply (:.$) SndSym0) UnPPSym0) a_1627678509 

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 (Let1627711705GoSym2 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.

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.

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

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.

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

The radical of a PrimePower type's value.

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

The odd radical of a PrimePower type's value.

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

The "hat" of a PrimePower type's value: \( p^e \) if \( p \) is odd, \( 2^{e-1} \) otherwise.

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

The value of a PrimeBin type.

Data-level equivalents of reflections for Factored data

valueF :: Factored -> Int Source #

The value of a Factored.

totientF :: Factored -> Int Source #

Totient of a Factored.

radicalF :: Factored -> Int Source #

The radical of a Factored.

oddRadicalF :: Factored -> Int Source #

The odd radical of a Factored.

valueHatF :: Factored -> Int Source #

The hat of a Factored.

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.

valueHatPP :: PP -> Int Source #

The "hat" of a prime power: \( p^e \) if \( p \) is odd, \( 2^{e-1} \) otherwise.

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 #

SOrd Pos Source # 

Methods

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

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

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

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

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

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

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

SEq Pos Source # 

Methods

(%:==) :: Sing Pos a -> Sing Pos b -> Sing Bool ((Pos :== a) b) #

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

SDecide Pos Source # 

Methods

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

SingKind Pos Source # 

Associated Types

type DemoteRep Pos :: * #

SingI Pos O Source # 

Methods

sing :: Sing O a #

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

Methods

sing :: Sing (S n0) a #

POrd Pos (Proxy * Pos) Source # 

Associated Types

type Compare (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: Ordering #

type ((Proxy * Pos) :< (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool #

type ((Proxy * Pos) :<= (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool #

type ((Proxy * Pos) :> (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool #

type ((Proxy * Pos) :>= (arg0 :: Proxy * Pos)) (arg1 :: Proxy * Pos) :: Bool #

type Max (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: a0 #

type Min (Proxy * Pos) (arg0 :: Proxy * Pos) (arg1 :: Proxy * Pos) :: a0 #

PEq Pos (Proxy * Pos) Source # 

Associated Types

type ((Proxy * Pos) :== (x :: Proxy * Pos)) (y :: Proxy * Pos) :: Bool #

type ((Proxy * Pos) :/= (x :: Proxy * Pos)) (y :: Proxy * Pos) :: Bool #

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 DemoteRep Pos Source # 
type Min Pos arg0 arg1 Source # 
type Min Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Min_1627688153Sym0 Pos) arg0) arg1
type Max Pos arg0 arg1 Source # 
type Max Pos arg0 arg1 = Apply Pos Pos (Apply Pos (TyFun Pos Pos -> Type) (Max_1627688120Sym0 Pos) arg0) arg1
type (:>=) Pos arg0 arg1 Source # 
type (:>=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688087Sym0 Pos) arg0) arg1
type (:>) Pos arg0 arg1 Source # 
type (:>) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688054Sym0 Pos) arg0) arg1
type (:<=) Pos arg0 arg1 Source # 
type (:<=) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627688021Sym0 Pos) arg0) arg1
type (:<) Pos arg0 arg1 Source # 
type (:<) Pos arg0 arg1 = Apply Pos Bool (Apply Pos (TyFun Pos Bool -> Type) (TFHelper_1627687988Sym0 Pos) arg0) arg1
type Compare Pos a1 a0 Source # 
type Compare Pos a1 a0
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 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 (NonEmpty a0) 
data Sing (NonEmpty a0) where
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing ((~>) k1 k2) 
data Sing ((~>) k1 k2) = SLambda {}
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.

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

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.

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

Convert a Pos to an integral type.

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

Convert an integral type to a Pos.

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_1627625799 = Apply ErrorSym0 "Invalid call to subPos: a <= b" 

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 #

SOrd Bin Source # 

Methods

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

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

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

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

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

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

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

SEq Bin Source # 

Methods

(%:==) :: Sing Bin a -> Sing Bin b -> Sing Bool ((Bin :== a) b) #

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

SDecide Bin Source # 

Methods

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

SingKind Bin Source # 

Associated Types

type DemoteRep Bin :: * #

SingI Bin B1 Source # 

Methods

sing :: Sing B1 a #

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 #

POrd Bin (Proxy * Bin) Source # 

Associated Types

type Compare (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: Ordering #

type ((Proxy * Bin) :< (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool #

type ((Proxy * Bin) :<= (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool #

type ((Proxy * Bin) :> (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool #

type ((Proxy * Bin) :>= (arg0 :: Proxy * Bin)) (arg1 :: Proxy * Bin) :: Bool #

type Max (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: a0 #

type Min (Proxy * Bin) (arg0 :: Proxy * Bin) (arg1 :: Proxy * Bin) :: a0 #

PEq Bin (Proxy * Bin) Source # 

Associated Types

type ((Proxy * Bin) :== (x :: Proxy * Bin)) (y :: Proxy * Bin) :: Bool #

type ((Proxy * Bin) :/= (x :: Proxy * Bin)) (y :: Proxy * Bin) :: Bool #

SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0 Source # 
SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0 Source # 
data Sing Bin Source # 
data Sing Bin where
type DemoteRep Bin Source # 
type Min Bin arg0 arg1 Source # 
type Min Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Min_1627688153Sym0 Bin) arg0) arg1
type Max Bin arg0 arg1 Source # 
type Max Bin arg0 arg1 = Apply Bin Bin (Apply Bin (TyFun Bin Bin -> Type) (Max_1627688120Sym0 Bin) arg0) arg1
type (:>=) Bin arg0 arg1 Source # 
type (:>=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688087Sym0 Bin) arg0) arg1
type (:>) Bin arg0 arg1 Source # 
type (:>) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688054Sym0 Bin) arg0) arg1
type (:<=) Bin arg0 arg1 Source # 
type (:<=) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627688021Sym0 Bin) arg0) arg1
type (:<) Bin arg0 arg1 Source # 
type (:<) Bin arg0 arg1 = Apply Bin Bool (Apply Bin (TyFun Bin Bool -> Type) (TFHelper_1627687988Sym0 Bin) arg0) arg1
type Compare Bin a1 a0 Source # 
type Compare Bin a1 a0
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

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 (NonEmpty a0) 
data Sing (NonEmpty a0) where
data Sing (Either a0 b0) 
data Sing (Either a0 b0) where
data Sing (a0, b0) 
data Sing (a0, b0) where
data Sing ((~>) k1 k2) 
data Sing ((~>) k1 k2) = SLambda {}
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.

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

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.

intToBin :: C z => z -> Bin Source #

Convert an integral type to a Bin.

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 (S (S (S O)))), PP '(P (D1 (D1 B1)), O)] Source #

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

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

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

type F228 = F '[PP '(P (D0 B1), S O), PP '(P (D1 B1), O), PP '(P (D1 (D1 (