lol-0.7.0.0: A library for lattice cryptography.

Copyright(c) Eric Crockett 2011-2017
Chris Peikert 2011-2017
LicenseGPL-3
Maintainerecrockett0@gmail.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 # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

Show Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Factored -> ShowS #

show :: Factored -> String #

showList :: [Factored] -> ShowS #

PShow Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol #

type Show_ arg :: Symbol #

type ShowList arg arg1 :: Symbol #

SShow [PrimePower] => SShow Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) #

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) #

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #

SEq [PrimePower] => SEq Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

PEq Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide [PrimePower] => SDecide Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

SingKind Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Demote Factored = (r :: Type) #

Methods

fromSing :: Sing a -> Demote Factored #

toSing :: Demote Factored -> SomeSing Factored #

(Fact m, C i) => Reflects (m :: Factored) i Source # 
Instance details

Defined in Crypto.Lol.Reflects

Methods

value :: i Source #

ShowSing [PrimePower] => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

Fact m => Show (ArgType m) Source # 
Instance details

Defined in Crypto.Lol.Utils.ShowType

Methods

showsPrec :: Int -> ArgType m -> ShowS #

show :: ArgType m -> String #

showList :: [ArgType m] -> ShowS #

data Sing (a :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where
type Demote Factored Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Demote Factored = Factored
type Show_ (arg :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Show_ (arg :: Factored) = Apply (Show__6989586621680262717Sym0 :: TyFun Factored Symbol -> Type) arg
type ShowList (arg :: [Factored]) arg1 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowList (arg :: [Factored]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [Factored] (Symbol ~> Symbol) -> Type) arg) arg1
type (x :: Factored) /= (y :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (x :: Factored) /= (y :: Factored) = Not (x == y)
type (a :: Factored) == (b :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (a :: Factored) == (b :: Factored)
type ShowsPrec a1 (a2 :: Factored) a3 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowsPrec a1 (a2 :: Factored) a3

type SFactored = (Sing :: Factored -> Type) Source #

type Fact (m :: Factored) = 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

newtype PrimePower Source #

Constructors

PP (PrimeBin, Pos) 
Instances
Eq PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

Show PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> PrimePower -> ShowS #

show :: PrimePower -> String #

showList :: [PrimePower] -> ShowS #

PShow PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol #

type Show_ arg :: Symbol #

type ShowList arg arg1 :: Symbol #

SShow (PrimeBin, Pos) => SShow PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) #

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) #

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #

SEq (PrimeBin, Pos) => SEq PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

PEq PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide (PrimeBin, Pos) => SDecide PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

SingKind PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Demote PrimePower = (r :: Type) #

Methods

fromSing :: Sing a -> Demote PrimePower #

toSing :: Demote PrimePower -> SomeSing PrimePower #

(PPow pp, C i) => Reflects (pp :: PrimePower) i Source # 
Instance details

Defined in Crypto.Lol.Reflects

Methods

value :: i Source #

SingI n => SingI (PP n :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (PP n) #

ShowSing (PrimeBin, Pos) => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

SingI (TyCon1 PP) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (TyCon1 PP) #

data Sing (a :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where
type Demote PrimePower Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Demote PrimePower = PrimePower
type Show_ (arg :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Show_ (arg :: PrimePower) = Apply (Show__6989586621680262717Sym0 :: TyFun PrimePower Symbol -> Type) arg
type ShowList (arg :: [PrimePower]) arg1 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowList (arg :: [PrimePower]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [PrimePower] (Symbol ~> Symbol) -> Type) arg) arg1
type (x :: PrimePower) /= (y :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (x :: PrimePower) /= (y :: PrimePower) = Not (x == y)
type (a :: PrimePower) == (b :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (a :: PrimePower) == (b :: PrimePower)
type ShowsPrec a1 (a2 :: PrimePower) a3 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowsPrec a1 (a2 :: PrimePower) a3

type SPrimePower = (Sing :: PrimePower -> Type) Source #

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

The singleton kind-indexed data family.

Instances
ShowSing Pos => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (PrimeBin, Pos) => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing [PrimePower] => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

data Sing (a :: Bool) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Pos) where
data Sing (a :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Bin) where
data Sing (a :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimeBin) where
data Sing (a :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where
data Sing (a :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where
data Sing (a :: Void) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (b :: [a]) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall a (b :: [a]). Sing ([] :: [a])
  • SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (b :: Min a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (b :: Endo a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where
data Sing (b :: MaxInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where
data Sing (b :: MinInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where
data Sing (c :: Either a b) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (b :: StateL s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where
  • SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where
  • SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
  • STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
  • STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where
  • STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

type PPow (pp :: PrimePower) = 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 # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

Ord PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

compare :: PrimeBin -> PrimeBin -> Ordering #

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

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

(>) :: PrimeBin -> PrimeBin -> Bool #

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

max :: PrimeBin -> PrimeBin -> PrimeBin #

min :: PrimeBin -> PrimeBin -> PrimeBin #

Show PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> PrimeBin -> ShowS #

show :: PrimeBin -> String #

showList :: [PrimeBin] -> ShowS #

PShow PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol #

type Show_ arg :: Symbol #

type ShowList arg arg1 :: Symbol #

SShow Bin => SShow PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) #

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) #

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #

POrd PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

SOrd Bin => SOrd PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SEq Bin => SEq PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

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

PEq PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide Bin => SDecide PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

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

SingKind PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Demote PrimeBin = (r :: Type) #

Methods

fromSing :: Sing a -> Demote PrimeBin #

toSing :: Demote PrimeBin -> SomeSing PrimeBin #

(Prime p, C i) => Reflects (p :: PrimeBin) i Source # 
Instance details

Defined in Crypto.Lol.Reflects

Methods

value :: i Source #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

SingI (TyCon1 PP) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (TyCon1 PP) #

data Sing (a :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimeBin) where
type Demote PrimeBin Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Demote PrimeBin = PrimeBin
type Show_ (arg :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Show_ (arg :: PrimeBin) = Apply (Show__6989586621680262717Sym0 :: TyFun PrimeBin Symbol -> Type) arg
type ShowList (arg :: [PrimeBin]) arg1 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowList (arg :: [PrimeBin]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [PrimeBin] (Symbol ~> Symbol) -> Type) arg) arg1
type Min (arg :: PrimeBin) (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Min (arg :: PrimeBin) (arg1 :: PrimeBin) = Apply (Apply (Min_6989586621679380222Sym0 :: TyFun PrimeBin (PrimeBin ~> PrimeBin) -> Type) arg) arg1
type Max (arg :: PrimeBin) (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Max (arg :: PrimeBin) (arg1 :: PrimeBin) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun PrimeBin (PrimeBin ~> PrimeBin) -> Type) arg) arg1
type (arg :: PrimeBin) >= (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (arg :: PrimeBin) >= (arg1 :: PrimeBin) = Apply (Apply (TFHelper_6989586621679380186Sym0 :: TyFun PrimeBin (PrimeBin ~> Bool) -> Type) arg) arg1
type (arg :: PrimeBin) > (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (arg :: PrimeBin) > (arg1 :: PrimeBin) = Apply (Apply (TFHelper_6989586621679380168Sym0 :: TyFun PrimeBin (PrimeBin ~> Bool) -> Type) arg) arg1
type (arg :: PrimeBin) <= (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (arg :: PrimeBin) <= (arg1 :: PrimeBin) = Apply (Apply (TFHelper_6989586621679380150Sym0 :: TyFun PrimeBin (PrimeBin ~> Bool) -> Type) arg) arg1
type (arg :: PrimeBin) < (arg1 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (arg :: PrimeBin) < (arg1 :: PrimeBin) = Apply (Apply (TFHelper_6989586621679380132Sym0 :: TyFun PrimeBin (PrimeBin ~> Bool) -> Type) arg) arg1
type Compare (a1 :: PrimeBin) (a2 :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type Compare (a1 :: PrimeBin) (a2 :: PrimeBin)
type (x :: PrimeBin) /= (y :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (x :: PrimeBin) /= (y :: PrimeBin) = Not (x == y)
type (a :: PrimeBin) == (b :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type (a :: PrimeBin) == (b :: PrimeBin)
type ShowsPrec a1 (a2 :: PrimeBin) a3 Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

type ShowsPrec a1 (a2 :: PrimeBin) a3

type SPrimeBin = (Sing :: PrimeBin -> Type) Source #

type Prime (p :: PrimeBin) = 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

pToPP :: PrimeBin -> PrimePower Source #

sPToPP :: forall (t :: PrimeBin). 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) 

ppToF :: PrimePower -> Factored Source #

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

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

Equations

PpToF pp = Apply FSym0 (Apply (Apply (:@#@$) pp) '[]) 

pToF :: PrimeBin -> Factored Source #

sPToF :: forall (t :: PrimeBin). Sing t -> Sing (Apply PToFSym0 t :: Factored) Source #

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

Equations

PToF a_6989586621679226325 = Apply (Apply (Apply (.@#@$) PpToFSym0) PToPPSym0) a_6989586621679226325 

Unwrappers

unF :: Factored -> [PrimePower] Source #

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

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

Equations

UnF (F pps) = pps 

unPP :: PrimePower -> (PrimeBin, Pos) Source #

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

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

Equations

UnPP (PP pp) = pp 

primePP :: PrimePower -> PrimeBin Source #

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

Equations

PrimePP a_6989586621679211408 = Apply (Apply (Apply (.@#@$) FstSym0) UnPPSym0) a_6989586621679211408 

exponentPP :: PrimePower -> Pos Source #

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

Equations

ExponentPP a_6989586621679211413 = Apply (Apply (Apply (.@#@$) SndSym0) UnPPSym0) a_6989586621679211413 

Arithmetic operations

fPPMul :: PrimePower -> Factored -> Factored Source #

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

Equations

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

fMul :: Factored -> Factored -> Factored Source #

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.

fDivides :: Factored -> Factored -> Bool Source #

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.

fDiv :: Factored -> Factored -> Factored Source #

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.

fGCD :: Factored -> Factored -> Factored Source #

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

Equations

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

fLCM :: Factored -> Factored -> Factored Source #

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.

fOddRadical :: Factored -> Factored Source #

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

Equations

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

pFree :: PrimeBin -> Factored -> Factored Source #

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

Equations

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

Reflections

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

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

valueFact :: forall m. Fact m => Int Source #

The value of a Factored type.

totientFact :: forall m. Fact m => Int Source #

The totient of a Factored type's value.

radicalFact :: forall m. Fact m => Int Source #

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

oddRadicalFact :: forall m. Fact m => Int Source #

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

valueHatFact :: forall m. Fact 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 => PP Source #

Reflect a PrimePower type to a PP value.

primePPow :: forall pp. PPow pp => Int Source #

Reflect the prime component of a PrimePower type.

exponentPPow :: forall pp. PPow pp => Int Source #

Reflect the exponent component of a PrimePower type.

valuePPow :: forall pp. PPow pp => Int Source #

The value of a PrimePower type.

totientPPow :: forall pp. PPow pp => Int Source #

The totient of a PrimePower type's value.

radicalPPow :: forall pp. PPow pp => Int Source #

The radical of a PrimePower type's value.

oddRadicalPPow :: forall pp. PPow pp => Int Source #

The odd radical of a PrimePower type's value.

valueHatPPow :: forall pp. PPow 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 => Int Source #

The value of a PrimeBin type.

Operations on Factored values

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. (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. (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. (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 m l. (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. (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'. (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') \).

(\\) :: HasDict c e => (c -> r) -> e -> r infixl 1 #

Operator version of withDict, with the arguments flipped

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 # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

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

Ord Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

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 # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Pos -> ShowS #

show :: Pos -> String #

showList :: [Pos] -> ShowS #

PShow Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol #

type Show_ arg :: Symbol #

type ShowList arg arg1 :: Symbol #

SShow Pos => SShow Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) #

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) #

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #

POrd Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

SOrd Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SEq Pos => SEq Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

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

PEq Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide Pos => SDecide Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

SingKind Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type Demote Pos = (r :: Type) #

Methods

fromSing :: Sing a -> Demote Pos #

toSing :: Demote Pos -> SomeSing Pos #

SingI O Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing O #

(PosC a, C i) => Reflects (a :: Pos) i Source # 
Instance details

Defined in Crypto.Lol.Reflects

Methods

value :: i Source #

SingI n => SingI (S n :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (S n) #

ShowSing Pos => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

SuppressUnusedWarnings SSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SuppressUnusedWarnings AddPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SuppressUnusedWarnings SubPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI SSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing SSym0 #

SingI AddPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing AddPosSym0 #

SingI SubPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing SubPosSym0 #

SuppressUnusedWarnings (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SuppressUnusedWarnings (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (AddPosSym1 d :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (AddPosSym1 d) #

SingI d => SingI (SubPosSym1 d :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (SubPosSym1 d) #

SingI (TyCon1 PP) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (TyCon1 PP) #

SingI (TyCon1 S) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (TyCon1 S) #

data Sing (a :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Pos) where
type Demote Pos Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Demote Pos = Pos
type Show_ (arg :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Show_ (arg :: Pos) = Apply (Show__6989586621680262717Sym0 :: TyFun Pos Symbol -> Type) arg
type ShowList (arg :: [Pos]) arg1 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type ShowList (arg :: [Pos]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [Pos] (Symbol ~> Symbol) -> Type) arg) arg1
type Min (arg :: Pos) (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Min (arg :: Pos) (arg1 :: Pos) = Apply (Apply (Min_6989586621679380222Sym0 :: TyFun Pos (Pos ~> Pos) -> Type) arg) arg1
type Max (arg :: Pos) (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Max (arg :: Pos) (arg1 :: Pos) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Pos (Pos ~> Pos) -> Type) arg) arg1
type (arg :: Pos) >= (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Pos) >= (arg1 :: Pos) = Apply (Apply (TFHelper_6989586621679380186Sym0 :: TyFun Pos (Pos ~> Bool) -> Type) arg) arg1
type (arg :: Pos) > (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Pos) > (arg1 :: Pos) = Apply (Apply (TFHelper_6989586621679380168Sym0 :: TyFun Pos (Pos ~> Bool) -> Type) arg) arg1
type (arg :: Pos) <= (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Pos) <= (arg1 :: Pos) = Apply (Apply (TFHelper_6989586621679380150Sym0 :: TyFun Pos (Pos ~> Bool) -> Type) arg) arg1
type (arg :: Pos) < (arg1 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Pos) < (arg1 :: Pos) = Apply (Apply (TFHelper_6989586621679380132Sym0 :: TyFun Pos (Pos ~> Bool) -> Type) arg) arg1
type Compare (a1 :: Pos) (a2 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Compare (a1 :: Pos) (a2 :: Pos)
type (x :: Pos) /= (y :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (x :: Pos) /= (y :: Pos) = Not (x == y)
type (a :: Pos) == (b :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (a :: Pos) == (b :: Pos)
type ShowsPrec a1 (a2 :: Pos) a3 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type ShowsPrec a1 (a2 :: Pos) a3
type Apply SSym0 (t6989586621679097999 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply SSym0 (t6989586621679097999 :: Pos) = S t6989586621679097999
type Apply (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) (a6989586621679098009 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) (a6989586621679098009 :: Pos) = AddPos a6989586621679098008 a6989586621679098009
type Apply (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) (a6989586621679098002 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) (a6989586621679098002 :: Pos) = SubPos a6989586621679098001 a6989586621679098002
type Apply AddPosSym0 (a6989586621679098008 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply AddPosSym0 (a6989586621679098008 :: Pos) = AddPosSym1 a6989586621679098008
type Apply SubPosSym0 (a6989586621679098001 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply SubPosSym0 (a6989586621679098001 :: Pos) = SubPosSym1 a6989586621679098001

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

The singleton kind-indexed data family.

Instances
ShowSing Pos => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (PrimeBin, Pos) => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing [PrimePower] => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

data Sing (a :: Bool) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Pos) where
data Sing (a :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Bin) where
data Sing (a :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimeBin) where
data Sing (a :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where
data Sing (a :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where
data Sing (a :: Void) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (b :: [a]) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall a (b :: [a]). Sing ([] :: [a])
  • SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (b :: Min a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (b :: Endo a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where
data Sing (b :: MaxInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where
data Sing (b :: MinInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where
data Sing (c :: Either a b) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (b :: StateL s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where
  • SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where
  • SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
  • STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
  • STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where
  • STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

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

type PosC (p :: Pos) = 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.

addPos :: Pos -> Pos -> Pos Source #

sAddPos :: forall (t :: Pos) (t :: Pos). 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) 

subPos :: Pos -> Pos -> Pos Source #

sSubPos :: forall (t :: Pos) (t :: Pos). 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 _ = Apply ErrorSym0 "Invalid call to subPos: a <= b" 

type OSym0 = O Source #

data SSym0 :: (~>) Pos Pos Source #

Instances
SuppressUnusedWarnings SSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI SSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing SSym0 #

type Apply SSym0 (t6989586621679097999 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply SSym0 (t6989586621679097999 :: Pos) = S t6989586621679097999

type SSym1 (t6989586621679097999 :: Pos) = S t6989586621679097999 Source #

data AddPosSym0 :: (~>) Pos ((~>) Pos Pos) Source #

Instances
SuppressUnusedWarnings AddPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI AddPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing AddPosSym0 #

type Apply AddPosSym0 (a6989586621679098008 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply AddPosSym0 (a6989586621679098008 :: Pos) = AddPosSym1 a6989586621679098008

data AddPosSym1 (a6989586621679098008 :: Pos) :: (~>) Pos Pos Source #

Instances
SuppressUnusedWarnings (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (AddPosSym1 d :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (AddPosSym1 d) #

type Apply (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) (a6989586621679098009 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply (AddPosSym1 a6989586621679098008 :: TyFun Pos Pos -> Type) (a6989586621679098009 :: Pos) = AddPos a6989586621679098008 a6989586621679098009

data SubPosSym0 :: (~>) Pos ((~>) Pos Pos) Source #

Instances
SuppressUnusedWarnings SubPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI SubPosSym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing SubPosSym0 #

type Apply SubPosSym0 (a6989586621679098001 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply SubPosSym0 (a6989586621679098001 :: Pos) = SubPosSym1 a6989586621679098001

data SubPosSym1 (a6989586621679098001 :: Pos) :: (~>) Pos Pos Source #

Instances
SuppressUnusedWarnings (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI d => SingI (SubPosSym1 d :: TyFun Pos Pos -> Type) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (SubPosSym1 d) #

type Apply (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) (a6989586621679098002 :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply (SubPosSym1 a6989586621679098001 :: TyFun Pos Pos -> Type) (a6989586621679098002 :: Pos) = SubPos a6989586621679098001 a6989586621679098002

Positive naturals in binary representation

data Bin Source #

Constructors

B1 
D0 Bin 
D1 Bin 
Instances
Eq Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

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

Ord Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

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 # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Bin -> ShowS #

show :: Bin -> String #

showList :: [Bin] -> ShowS #

PShow Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol #

type Show_ arg :: Symbol #

type ShowList arg arg1 :: Symbol #

SShow Bin => SShow Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) #

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) #

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #

POrd Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type Compare arg arg1 :: Ordering #

type arg < arg1 :: Bool #

type arg <= arg1 :: Bool #

type arg > arg1 :: Bool #

type arg >= arg1 :: Bool #

type Max arg arg1 :: a #

type Min arg arg1 :: a #

SOrd Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) #

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) #

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) #

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) #

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) #

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) #

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #

SEq Bin => SEq Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

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

PEq Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide Bin => SDecide Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

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

SingKind Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Associated Types

type Demote Bin = (r :: Type) #

Methods

fromSing :: Sing a -> Demote Bin #

toSing :: Demote Bin -> SomeSing Bin #

SingI B1 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing B1 #

(BinC a, C i) => Reflects (a :: Bin) i Source # 
Instance details

Defined in Crypto.Lol.Reflects

Methods

value :: i Source #

SingI n => SingI (D0 n :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (D0 n) #

SingI n => SingI (D1 n :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (D1 n) #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

SuppressUnusedWarnings D1Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SuppressUnusedWarnings D0Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI D1Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing D1Sym0 #

SingI D0Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing D0Sym0 #

SingI (TyCon1 D0) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (TyCon1 D0) #

SingI (TyCon1 D1) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing (TyCon1 D1) #

data Sing (a :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Bin) where
type Demote Bin Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Demote Bin = Bin
type Show_ (arg :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Show_ (arg :: Bin) = Apply (Show__6989586621680262717Sym0 :: TyFun Bin Symbol -> Type) arg
type ShowList (arg :: [Bin]) arg1 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type ShowList (arg :: [Bin]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [Bin] (Symbol ~> Symbol) -> Type) arg) arg1
type Min (arg :: Bin) (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Min (arg :: Bin) (arg1 :: Bin) = Apply (Apply (Min_6989586621679380222Sym0 :: TyFun Bin (Bin ~> Bin) -> Type) arg) arg1
type Max (arg :: Bin) (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Max (arg :: Bin) (arg1 :: Bin) = Apply (Apply (Max_6989586621679380204Sym0 :: TyFun Bin (Bin ~> Bin) -> Type) arg) arg1
type (arg :: Bin) >= (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Bin) >= (arg1 :: Bin) = Apply (Apply (TFHelper_6989586621679380186Sym0 :: TyFun Bin (Bin ~> Bool) -> Type) arg) arg1
type (arg :: Bin) > (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Bin) > (arg1 :: Bin) = Apply (Apply (TFHelper_6989586621679380168Sym0 :: TyFun Bin (Bin ~> Bool) -> Type) arg) arg1
type (arg :: Bin) <= (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Bin) <= (arg1 :: Bin) = Apply (Apply (TFHelper_6989586621679380150Sym0 :: TyFun Bin (Bin ~> Bool) -> Type) arg) arg1
type (arg :: Bin) < (arg1 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (arg :: Bin) < (arg1 :: Bin) = Apply (Apply (TFHelper_6989586621679380132Sym0 :: TyFun Bin (Bin ~> Bool) -> Type) arg) arg1
type Compare (a1 :: Bin) (a2 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Compare (a1 :: Bin) (a2 :: Bin)
type (x :: Bin) /= (y :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (x :: Bin) /= (y :: Bin) = Not (x == y)
type (a :: Bin) == (b :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type (a :: Bin) == (b :: Bin)
type ShowsPrec a1 (a2 :: Bin) a3 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type ShowsPrec a1 (a2 :: Bin) a3
type Apply D1Sym0 (t6989586621679155375 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply D1Sym0 (t6989586621679155375 :: Bin) = D1 t6989586621679155375
type Apply D0Sym0 (t6989586621679155373 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply D0Sym0 (t6989586621679155373 :: Bin) = D0 t6989586621679155373

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

The singleton kind-indexed data family.

Instances
ShowSing Pos => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing Bin => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing (PrimeBin, Pos) => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

ShowSing [PrimePower] => Show (Sing z) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS #

show :: Sing z -> String #

showList :: [Sing z] -> ShowS #

data Sing (a :: Bool) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Pos) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Pos) where
data Sing (a :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Bin) where
data Sing (a :: PrimeBin) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimeBin) where
data Sing (a :: PrimePower) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where
data Sing (a :: Factored) Source # 
Instance details

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where
data Sing (a :: Void) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (b :: [a]) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall a (b :: [a]). Sing ([] :: [a])
  • SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (b :: Min a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (b :: Endo a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where
data Sing (b :: MaxInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where
data Sing (b :: MinInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where
data Sing (c :: Either a b) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (b :: StateL s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where
  • SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where
  • SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
  • STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
  • STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where
  • STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

type SBin = (Sing :: Bin -> Type) Source #

type BinC (b :: Bin) = 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 #

data D0Sym0 :: (~>) Bin Bin Source #

Instances
SuppressUnusedWarnings D0Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI D0Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing D0Sym0 #

type Apply D0Sym0 (t6989586621679155373 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply D0Sym0 (t6989586621679155373 :: Bin) = D0 t6989586621679155373

type D0Sym1 (t6989586621679155373 :: Bin) = D0 t6989586621679155373 Source #

data D1Sym0 :: (~>) Bin Bin Source #

Instances
SuppressUnusedWarnings D1Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

suppressUnusedWarnings :: () #

SingI D1Sym0 Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

Methods

sing :: Sing D1Sym0 #

type Apply D1Sym0 (t6989586621679155375 :: Bin) Source # 
Instance details

Defined in Crypto.Lol.PosBinDefs

type Apply D1Sym0 (t6989586621679155375 :: Bin) = D1 t6989586621679155375

type D1Sym1 (t6989586621679155375 :: Bin) = D1 t6989586621679155375 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 P64 = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type P17 = S (S (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 P15 = S (S (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 P13 = S (S (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 P11 = S (S (S (S (S (S (S (S (S (S O))))))))) Source #

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

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

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

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

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

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

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

type P3 = S (S O) Source #

type P2 = S O Source #

type P1 = O Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type B7 = D1 (D1 B1) Source #

type B6 = D0 (D1 B1) Source #

type B5 = D1 (D0 B1) Source #

type B4 = D0 (D0 B1) Source #

type B3 = D1 B1 Source #

type B2 = D0 B1 Source #

type B1 = B1 Source #

Convenient synonyms for Factored, PrimePower, and Prime types

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type F229 = F '[PP '(P (D1 (D0 (D1 (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 (D0 (D0 B1)))), O)] Source #

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

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

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

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

type F223 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D0 (D1 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 F221 = F '[PP '(P (D1 (D0 (D1 B1))), O), PP '(P (D1 (D0 (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 F219 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))), O)] Source #

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

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

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

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

type F214 = F '[PP '(P (D0 B1), O), PP '(P (D1 (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 F212 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D0 (D1 B1))))), O)] Source #

type F211 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 (D1 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 F209 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D1 (D0 (D0 B1)))), O)] Source #

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

type F207 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (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 F205 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (D1 (D0 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 F203 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

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

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

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

type F199 = F '[PP '(P (D1 (D1 (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 F197 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))), O)] Source #

type F196 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 B1)), S 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 F194 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))), O)] Source #

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

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

type F191 = F '[PP '(P (D1 (D1 (D1 (D1 (D1 (D1 (D0 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 F189 = F '[PP '(P (D1 B1), S (S O)), PP '(P (D1 (D1 B1)), O)] Source #

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

type F187 = F '[PP '(P (D1 (D1 (D0 B1))), O), PP '(P (D1 (D0 (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 F185 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 (D0 (D0 B1))))), O)] Source #

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

type F183 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 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 F181 = F '[PP '(P (D1 (D0 (D1 (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 F179 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))), O)] Source #

type F178 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D0 (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 F176 = F '[PP '(P (D0 B1), S (S (S O))), PP '(P (D1 (D1 (D0 B1))), O)] Source #

type F175 = F '[PP '(P (D1 (D0 B1)), S O), PP '(P (D1 (D1 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 F173 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))), O)] Source #

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

type F171 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D1 (D0 (D0 B1)))), 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 F169 = F '[PP '(P (D1 (D0 (D1 B1))), S 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 F167 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (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 F165 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 B1)), O), PP '(P (D1 (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 F163 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))), O)] Source #

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

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

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

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

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

type F157 = F '[PP '(P (D1 (D0 (D1 (D1 (D1 (D0 (D0 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 F155 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D1 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 F153 = F '[PP '(P (D1 B1), S O), PP '(P (D1 (D0 (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 F151 = F '[PP '(P (D1 (D1 (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 F149 = F '[PP '(P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))), O)] Source #

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

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

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

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

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

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

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

type F141 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D1 (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 F139 = F '[PP '(P (D1 (D1 (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 F137 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))), O)] Source #

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

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

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

type F133 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (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 F131 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 (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 F129 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D0 (D1 (D0 B1))))), O)] Source #

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

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

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

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

type F124 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (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 F122 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (D1 (D1 (D1 B1))))), O)] Source #

type F121 = F '[PP '(P (D1 (D1 (D0 B1))), S 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 F119 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D0 (D0 B1)))), O)] Source #

type F118 = F '[PP '(P (D0 B1), O), PP '(P (D1 (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 F116 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

type F115 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D1 (D1 (D0 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 F113 = F '[PP '(P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))), O)] Source #

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

type F111 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D0 (D1 (D0 (D0 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 F109 = F '[PP '(P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))), O)] Source #

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

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

type F106 = F '[PP '(P (D0 B1), O), PP '(P (D1 (D0 (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 F104 = F '[PP '(P (D0 B1), S (S O)), PP '(P (D1 (D0 (D1 B1))), O)] Source #

type F103 = F '[PP '(P (D1 (D1 (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 F101 = F '[PP '(P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))), O)] Source #

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

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

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

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

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

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

type F94 = F '[PP '(P (D0 B1), O), PP '(P (D1 (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 F92 = F '[PP '(P (D0 B1), S O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

type F91 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D0 (D1 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 F89 = F '[PP '(P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))), O)] Source #

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

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

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

type F85 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D0 (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 F83 = F '[PP '(P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))), O)] Source #

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

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

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

type F79 = F '[PP '(P (D1 (D1 (D1 (D1 (D0 (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 F77 = F '[PP '(P (D1 (D1 B1)), O), PP '(P (D1 (D1 (D0 B1))), O)] Source #

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

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

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

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

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

type F71 = F '[PP '(P (D1 (D1 (D1 (D0 (D0 (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 F69 = F '[PP '(P (D1 B1), O), PP '(P (D1 (D1 (D1 (D0 B1)))), O)] Source #

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

type F67 = F '[PP '(P (D1 (D1 (D0 (D0 (D0 (D0 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 F65 = F '[PP '(P (D1 (D0 B1)), O), PP '(P (D1 (D0 (D1 B1))), O)] Source #

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

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

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

type F61 = F '[PP '(P (D1 (D0 (D1 (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 F59 = F '[PP '(P (D1 (D1 (D0 (D1 (D1 B1))))), O)] Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type F43 = F '[PP '(P (D1 (D1 (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 F41 = F '[PP '(P (D1 (D0 (D0 (D1 (D0 B1))))), O)] Source #

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

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

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

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

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

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

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

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

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

type F31 = F '[PP '(P (D1 (D1 (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 F29 = F '[PP '(P (D1 (D0 (D1 (D1 B1)))), O)] Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type F1 = F '[] Source #

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

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

type PP128 = PP '(P (D0 B1), S (S (S (S (S (S O)))))) Source #

type PP64 = PP '(P (D0 B1), S (S (S (S (S O))))) Source #

type PP32 = PP '(P (D0 B1), S (S (S (S O)))) Source #

type PP16 = PP '(P (D0 B1), S (S (S O))) Source #

type PP8 = PP '(P (D0 B1), S (S O)) Source #

type PP4 = PP '(P (D0 B1), S O) Source #

type PP2 = PP '(P (D0 B1), O) Source #

type PP81 = PP '(P (D1 B1), S (S (S O))) Source #

type PP27 = PP '(P (D1 B1), S (S O)) Source #

type PP9 = PP '(P (D1 B1), S O) Source #

type PP3 = PP '(P (D1 B1), O) Source #

type PP11 = PP '(P (D1 (D1 (D0 B1))), O) Source #

type PP7 = PP '(P (D1 (D1 B1)), O) Source #

type PP5 = PP '(P (D1 (D0 B1)), O) Source #

type Prime659 = P (D1 (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D0 B1))))))))) Source #

type Prime653 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source #

type Prime647 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source #

type Prime643 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source #

type Prime641 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D1 (D0 B1))))))))) Source #

type Prime631 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))))) Source #

type Prime619 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source #

type Prime617 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source #

type Prime613 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1))))))))) Source #

type Prime607 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime601 = P (D1 (D0 (D0 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime599 = P (D1 (D1 (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime593 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime587 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime577 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D0 (D0 B1))))))))) Source #

type Prime571 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source #

type Prime569 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source #

type Prime563 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1))))))))) Source #

type Prime557 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))))) Source #

type Prime547 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))))) Source #

type Prime541 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1))))))))) Source #

type Prime523 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))))) Source #

type Prime521 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))))) Source #

type Prime509 = P (D1 (D0 (D1 (D1 (D1 (D1 (D1 (D1 B1)))))))) Source #

type Prime503 = P (D1 (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1)))))))) Source #

type Prime499 = P (D1 (D1 (D0 (D0 (D1 (D1 (D1 (D1 B1)))))))) Source #

type Prime491 = P (D1 (D1 (D0 (D1 (D0 (D1 (D1 (D1 B1)))))))) Source #

type Prime487 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D1 B1)))))))) Source #

type Prime479 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1)))))))) Source #

type Prime467 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1)))))))) Source #

type Prime463 = P (D1 (D1 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source #

type Prime461 = P (D1 (D0 (D1 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source #

type Prime457 = P (D1 (D0 (D0 (D1 (D0 (D0 (D1 (D1 B1)))))))) Source #

type Prime449 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 (D1 B1)))))))) Source #

type Prime443 = P (D1 (D1 (D0 (D1 (D1 (D1 (D0 (D1 B1)))))))) Source #

type Prime439 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D1 B1)))))))) Source #

type Prime433 = P (D1 (D0 (D0 (D0 (D1 (D1 (D0 (D1 B1)))))))) Source #

type Prime431 = P (D1 (D1 (D1 (D1 (D0 (D1 (D0 (D1 B1)))))))) Source #

type Prime421 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D1 B1)))))))) Source #

type Prime419 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 (D1 B1)))))))) Source #

type Prime409 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D1 B1)))))))) Source #

type Prime401 = P (D1 (D0 (D0 (D0 (D1 (D0 (D0 (D1 B1)))))))) Source #

type Prime397 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D1 B1)))))))) Source #

type Prime389 = P (D1 (D0 (D1 (D0 (D0 (D0 (D0 (D1 B1)))))))) Source #

type Prime383 = P (D1 (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1)))))))) Source #

type Prime379 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 (D0 B1)))))))) Source #

type Prime373 = P (D1 (D0 (D1 (D0 (D1 (D1 (D1 (D0 B1)))))))) Source #

type Prime367 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 (D0 B1)))))))) Source #

type Prime359 = P (D1 (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1)))))))) Source #

type Prime353 = P (D1 (D0 (D0 (D0 (D0 (D1 (D1 (D0 B1)))))))) Source #

type Prime349 = P (D1 (D0 (D1 (D1 (D1 (D0 (D1 (D0 B1)))))))) Source #

type Prime347 = P (D1 (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1)))))))) Source #

type Prime337 = P (D1 (D0 (D0 (D0 (D1 (D0 (D1 (D0 B1)))))))) Source #

type Prime331 = P (D1 (D1 (D0 (D1 (D0 (D0 (D1 (D0 B1)))))))) Source #

type Prime317 = P (D1 (D0 (D1 (D1 (D1 (D1 (D0 (D0 B1)))))))) Source #

type Prime313 = P (D1 (D0 (D0 (D1 (D1 (D1 (D0 (D0 B1)))))))) Source #

type Prime311 = P (D1 (D1 (D1 (D0 (D1 (D1 (D0 (D0 B1)))))))) Source #

type Prime307 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 (D0 B1)))))))) Source #

type Prime293 = P (D1 (D0 (D1 (D0 (D0 (D1 (D0 (D0 B1)))))))) Source #

type Prime283 = P (D1 (D1 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))) Source #

type Prime281 = P (D1 (D0 (D0 (D1 (D1 (D0 (D0 (D0 B1)))))))) Source #

type Prime277 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 (D0 B1)))))))) Source #

type Prime271 = P (D1 (D1 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))) Source #

type Prime269 = P (D1 (D0 (D1 (D1 (D0 (D0 (D0 (D0 B1)))))))) Source #

type Prime263 = P (D1 (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1)))))))) Source #

type Prime257 = P (D1 (D0 (D0 (D0 (D0 (D0 (D0 (D0 B1)))))))) Source #

type Prime251 = P (D1 (D1 (D0 (D1 (D1 (D1 (D1 B1))))))) Source #

type Prime241 = P (D1 (D0 (D0 (D0 (D1 (D1 (D1 B1))))))) Source #

type Prime239 = P (D1 (D1 (D1 (D1 (D0 (D1 (D1 B1))))))) Source #

type Prime233 = P (D1 (D0 (D0 (D1 (D0 (D1 (D1 B1))))))) Source #

type Prime229 = P (D1 (D0 (D1 (D0 (D0 (D1 (D1 B1))))))) Source #

type Prime227 = P (D1 (D1 (D0 (D0 (D0 (D1 (D1 B1))))))) Source #

type Prime223 = P (D1 (D1 (D1 (D1 (D1 (D0 (D1 B1))))))) Source #

type Prime211 = P (D1 (D1 (D0 (D0 (D1 (D0 (D1 B1))))))) Source #

type Prime199 = P (D1 (D1 (D1 (D0 (D0 (D0 (D1 B1))))))) Source #

type Prime197 = P (D1 (D0 (D1 (D0 (D0 (D0 (D1 B1))))))) Source #

type Prime193 = P (D1 (D0 (D0 (D0 (D0 (D0 (D1 B1))))))) Source #

type Prime191 = P (D1 (D1 (D1 (D1 (D1 (D1 (D0 B1))))))) Source #

type Prime181 = P (D1 (D0 (D1 (D0 (D1 (D1 (D0 B1))))))) Source #

type Prime179 = P (D1 (D1 (D0 (D0 (D1 (D1 (D0 B1))))))) Source #

type Prime173 = P (D1 (D0 (D1 (D1 (D0 (D1 (D0 B1))))))) Source #

type Prime167 = P (D1 (D1 (D1 (D0 (D0 (D1 (D0 B1))))))) Source #

type Prime163 = P (D1 (D1 (D0 (D0 (D0 (D1 (D0 B1))))))) Source #

type Prime157 = P (D1 (D0 (D1 (D1 (D1 (D0 (D0 B1))))))) Source #

type Prime151 = P (D1 (D1 (D1 (D0 (D1 (D0 (D0 B1))))))) Source #

type Prime149 = P (D1 (D0 (D1 (D0 (D1 (D0 (D0 B1))))))) Source #

type Prime139 = P (D1 (D1 (D0 (D1 (D0 (D0 (D0 B1))))))) Source #

type Prime137 = P (D1 (D0 (D0 (D1 (D0 (D0 (D0 B1))))))) Source #

type Prime131 = P (D1 (D1 (D0 (D0 (D0 (D0 (D0 B1))))))) Source #

type Prime127 = P (D1 (D1 (D1 (D1 (D1 (D1 B1)))))) Source #

type Prime113 = P (D1 (D0 (D0 (D0 (D1 (D1 B1)))))) Source #

type Prime109 = P (D1 (D0 (D1 (D1 (D0 (D1 B1)))))) Source #

type Prime107 = P (D1 (D1 (D0 (D1 (D0 (D1 B1)))))) Source #

type Prime103 = P (D1 (D1 (D1 (D0 (D0 (D1 B1)))))) Source #

type Prime101 = P (D1 (D0 (D1 (D0 (D0 (D1 B1)))))) Source #

type Prime97 = P (D1 (D0 (D0 (D0 (D0 (D1 B1)))))) Source #

type Prime89 = P (D1 (D0 (D0 (D1 (D1 (D0 B1)))))) Source #

type Prime83 = P (D1 (D1 (D0 (D0 (D1 (D0 B1)))))) Source #

type Prime79 = P (D1 (D1 (D1 (D1 (D0 (D0 B1)))))) Source #

type Prime73 = P (D1 (D0 (D0 (D1 (D0 (D0 B1)))))) Source #

type Prime71 = P (D1 (D1 (D1 (D0 (D0 (D0 B1)))))) Source #

type Prime67 = P (D1 (D1 (D0 (D0 (D0 (D0 B1)))))) Source #

type Prime61 = P (D1 (D0 (D1 (D1 (D1 B1))))) Source #

type Prime59 = P (D1 (D1 (D0 (D1 (D1 B1))))) Source #

type Prime53 = P (D1 (D0 (D1 (D0 (D1 B1))))) Source #

type Prime47 = P (D1 (D1 (D1 (D1 (D0 B1))))) Source #

type Prime43 = P (D1 (D1 (D0 (D1 (D0 B1))))) Source #

type Prime41 = P (D1 (D0 (D0 (D1 (D0 B1))))) Source #

type Prime37 = P (D1 (D0 (D1 (D0 (D0 B1))))) Source #

type Prime31 = P (D1 (D1 (D1 (D1 B1)))) Source #

type Prime29 = P (D1 (D0 (D1 (D1 B1)))) Source #

type Prime23 = P (D1 (D1 (D1 (D0 B1)))) Source #

type Prime19 = P (D1 (D1 (D0 (D0 B1)))) Source #

type Prime17 = P (D1 (D0 (D0 (D0 B1)))) Source #

type Prime13 = P (D1 (D0 (D1 B1))) Source #

type Prime11 = P (D1 (D1 (D0 B1))) Source #

type Prime7 = P (D1 (D1 B1)) Source #

type Prime5 = P (D1 (D0 B1)) Source #

type Prime3 = P (D1 B1) Source #

type Prime2 = P (D0 B1) Source #