lol-0.0.1.0: A library for lattice cryptography.

Safe HaskellNone
LanguageHaskell2010

Crypto.Lol.Factored

Contents

Description

This file defines types and operations for type-level representation and manipulation of factored integers. It relies on TH, so the documentation will be difficult to read. See comments for better documentation.

Synopsis

Factored natural numbers

type SFactored = (Sing :: Factored -> *) Source

type Fact m = SingI m Source

Kind-restricted synonym for SingI. Use this in constraints for types requiring a Factored type.

Prime powers

type PPow pp = SingI pp Source

Kind-restricted synonym for SingI. Use this in constraints for types requiring a PrimePower type.

data family Sing a

The singleton kind-indexed data family.

Instances

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

Naturals

data Nat :: *

Instances

Eq Nat 
Num Nat 
Ord Nat 
Show Nat 
SingI Nat Z 
(NatC a, Integral i) => Reflects Nat a i Source 
SingKind Nat (KProxy Nat) 
SingI Nat n0 => SingI Nat (S n0) 
PNum Nat (KProxy Nat) 
SNum Nat (KProxy Nat) 
POrd Nat (KProxy Nat) 
SOrd Nat (KProxy Nat) 
SEq Nat (KProxy Nat) 
PEq Nat (KProxy Nat) 
SDecide Nat (KProxy Nat) 
SuppressUnusedWarnings (TyFun Nat Nat -> *) FromInteger_1627442827Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> *) -> *) (:<<=$) 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> *) -> *) TFHelper_1627439202Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:**$) 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) TFHelper_1627442781Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) TFHelper_1627442756Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) TFHelper_1627442730Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) Min_1627439239Sym0 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) Max_1627439272Sym0 
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 
SuppressUnusedWarnings (TyFun Nat Nat -> *) Signum_1627442809Sym0 
SuppressUnusedWarnings (TyFun Nat Nat -> *) Abs_1627442796Sym0 
SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$) 
SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) TFHelper_1627439202Sym1 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:**$$) 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442781Sym1 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442756Sym1 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) TFHelper_1627442730Sym1 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) Min_1627439239Sym1 
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) Max_1627439272Sym1 
data Sing Nat where 
type FromInteger Nat a0 = Apply Nat Nat FromInteger_1627442827Sym0 a0 
type Signum Nat a0 = Apply Nat Nat Signum_1627442809Sym0 a0 
type Abs Nat a0 = Apply Nat Nat Abs_1627442796Sym0 a0 
type Negate Nat arg0 = Apply Nat Nat (Negate_1627753616Sym0 Nat) arg0 
type (:*) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442781Sym0 a0) a1 
type (:-) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442756Sym0 a0) a1 
type (:+) Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442730Sym0 a0) a1 
type Min Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat Min_1627439239Sym0 a0) a1 
type Max Nat a0 a1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat Max_1627439272Sym0 a0) a1 
type (:>=) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641632Sym0 Nat) arg0) arg1 
type (:>) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641599Sym0 Nat) arg0) arg1 
type (:<=) Nat a0 a1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat TFHelper_1627439202Sym0 a0) a1 
type (:<) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641533Sym0 Nat) arg0) arg1 
type Compare Nat arg0 arg1 = Apply Ordering Nat (Apply (TyFun Nat Ordering -> *) Nat (Compare_1627641500Sym0 Nat) arg0) arg1 
type (:/=) Nat x y = Not ((:==) Nat x y) 
type (:==) Nat a0 b0 = Equals_1627433666 a0 b0 
type Apply Nat Nat FromInteger_1627442827Sym0 l0 = FromInteger_1627442827Sym1 l0 
type Apply Nat Nat SSym0 l0 = SSym1 l0 
type Apply Nat Nat Signum_1627442809Sym0 l0 = Signum_1627442809Sym1 l0 
type Apply Nat Nat Abs_1627442796Sym0 l0 = Abs_1627442796Sym1 l0 
type Apply Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0 
type Apply Bool Nat (TFHelper_1627439202Sym1 l1) l0 = TFHelper_1627439202Sym2 l1 l0 
type Apply Nat Nat ((:**$$) l1) l0 = (:**$$$) l1 l0 
type Apply Nat Nat (TFHelper_1627442781Sym1 l1) l0 = TFHelper_1627442781Sym2 l1 l0 
type Apply Nat Nat (TFHelper_1627442756Sym1 l1) l0 = TFHelper_1627442756Sym2 l1 l0 
type Apply Nat Nat (TFHelper_1627442730Sym1 l1) l0 = TFHelper_1627442730Sym2 l1 l0 
type Apply Nat Nat (Min_1627439239Sym1 l1) l0 = Min_1627439239Sym2 l1 l0 
type Apply Nat Nat (Max_1627439272Sym1 l1) l0 = Max_1627439272Sym2 l1 l0 
type DemoteRep Nat (KProxy Nat) = Nat 
type MonomorphicRep Nat (Sing Nat) = Int 
type CharOf * (ZqBasic Nat p z) = p Source 
type Apply (TyFun Nat Bool -> *) Nat (:<<=$) l0 = (:<<=$$) l0 
type Apply (TyFun Nat Bool -> *) Nat TFHelper_1627439202Sym0 l0 = TFHelper_1627439202Sym1 l0 
type Apply (TyFun Nat Nat -> *) Nat (:**$) l0 = (:**$$) l0 
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442781Sym0 l0 = TFHelper_1627442781Sym1 l0 
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442756Sym0 l0 = TFHelper_1627442756Sym1 l0 
type Apply (TyFun Nat Nat -> *) Nat TFHelper_1627442730Sym0 l0 = TFHelper_1627442730Sym1 l0 
type Apply (TyFun Nat Nat -> *) Nat Min_1627439239Sym0 l0 = Min_1627439239Sym1 l0 
type Apply (TyFun Nat Nat -> *) Nat Max_1627439272Sym0 l0 = Max_1627439272Sym1 l0 

type NatC p = SingI p Source

Kind-restricted synonym for SingI. Use this in constraints for types requiring a Nat type.

type family PrimeNat a Source

Equations

PrimeNat arg_1627477538 = Case_1627478044 arg_1627477538 arg_1627477538 

type Prime p = (NatC p, PrimeNat p ~ True) Source

Constructors

sToPP :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ToPPSym0 t) t :: PrimePower) Source

type family ToPP a a :: PrimePower Source

Equations

ToPP arg_1627477532 arg_1627477534 = Case_1627478100 arg_1627477532 arg_1627477534 (Apply (Apply Tuple2Sym0 arg_1627477532) arg_1627477534) 

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

type family PpToF a :: Factored Source

Equations

PpToF pp = Apply FSym0 (Apply (Apply (:$) pp) `[]`) 

type PToF p = PpToF (ToPP p N1) Source

Type (family) synonym to create a Factored from a prime Nat

Unwrappers

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

type family UnF a :: [PrimePower] Source

Equations

UnF (F pps) = pps 

sUnPP :: forall t. Sing t -> Sing (Apply UnPPSym0 t :: (Nat, Nat)) Source

type family UnPP a :: (Nat, Nat) Source

Equations

UnPP (PP pp) = pp 

type family PrimePP a :: Nat Source

Equations

PrimePP a_1627454352 = Apply (Apply (Apply (:.$) FstSym0) UnPPSym0) a_1627454352 

type family ExponentPP a :: Nat Source

Equations

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

Arithmetic operations

type family FPPMul a a :: Factored Source

Equations

FPPMul (PP `(_z_1627464482, Z)`) y = y 
FPPMul (PP `(wild_1627464368, S wild_1627464370)`) (F pps) = Apply FSym0 (Apply (Apply PpMulSym0 (Let1627464489PpSym3 pps wild_1627464368 wild_1627464370)) pps) 

type family FMul a a :: Factored Source

Equations

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

type * a b = FMul a b Source

Type (family) synonym for multiplication of Factored types

type family FDivides a a :: Bool Source

Equations

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

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

Constraint synonym for divisibility of Factored types

type family FDiv a a :: Factored Source

Equations

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

type (/) a b = FDiv a b Source

Type (family) synonym for division of Factored types

type family FGCD a a :: Factored Source

Equations

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

type family FLCM a a :: Factored Source

Equations

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

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

Constraint synonym for coprimality of Factored types

type family FOddRadical a :: Factored Source

Equations

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

type family PFree a a :: Factored Source

Equations

PFree n (F pps) = Apply FSym0 (Apply (Let1627502537GoSym2 n pps) pps) 

Coercions

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

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

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

Entails constraint for divisibility by GCD, i.e. if g=GCD(m1,m2), then g|m1 and g|m2.

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

Entails constraint for LCM divisibility, i.e. if l=LCM(m1,m2), then m1|l and m2|l.

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

Entails constraint for LCM divisibility, i.e. the LCM of two divisors of m also divides m.

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

Entails basic facts for p-free division, i.e. if f is m after removing all p-factors, then f|m and gcd(f,p)=1

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

Entails basic facts for p-free division, i.e., if m|m', then p-free(m) | p-free(m')

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

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

Operations on factored integers and naturals

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

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

valueFact :: Fact m => Tagged m Int Source

Int representing the value of a Factored type

totientFact :: Fact m => Tagged m Int Source

Int representing the totient of a Factored type's value

valueHatFact :: Fact m => Tagged m Int Source

Int representing the "hat" of a Factored type's value m: m, if m is odd, or m/2 otherwise.

radicalFact :: Fact m => Tagged m Int Source

Int representing the radical (product of prime divisors) of a Factored type

oddRadicalFact :: Fact m => Tagged m Int Source

Int representing the odd radical (product of odd prime divisors) of a Factored type

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

Reflects a PrimePower type to a PP value

primePPow :: PPow pp => Tagged pp Int Source

Reflects the prime component of a PrimePower type

exponentPPow :: PPow pp => Tagged pp Int Source

Reflects the exponent component of a PrimePower type

valuePPow :: PPow pp => Tagged pp Int Source

Int representing the value of a PrimePower type

totientPPow :: PPow pp => Tagged pp Int Source

Int representing the totient of a PrimePower type's value

valueNatC :: forall p. NatC p => Tagged p Int Source

Int representing the value of a Nat

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

Returns m, if m is odd, or m/2 otherwise

type PP = (Int, Int) Source

Type synonym for (prime :: Int, exponent :: Int) pair

ppToPP :: PrimePower -> PP Source

Converts a Nat prime-power pair to an Int prime-power pair

valuePP :: PP -> Int Source

Evaluates a prime-power pair (p,e) to p^e

totientPP :: PP -> Int Source

Euler's totient function of a prime-power pair

radicalPP :: PP -> Int Source

The prime component of a prime-power pair

oddRadicalPP :: PP -> Int Source

The odd radical of a prime-power pair (p,_): p if p is odd, 1 if p==2

valuePPs :: [PP] -> Int Source

Product of values of individual PPs

totientPPs :: [PP] -> Int Source

Product of totients of individual PPs

radicalPPs :: [PP] -> Int Source

Product of radicals of individual PPs

oddRadicalPPs :: [PP] -> Int Source

Product of odd radicals of individual PPs

Type synonyms (not type families)

type family F1 Source

Equations

F1 = Apply FSym0 `[]` 

type family F2 Source

Equations

F2 = Apply PrimeToFSym0 N2Sym0 

type family F3 Source

Equations

F3 = Apply PrimeToFSym0 N3Sym0 

type family F4 Source

Equations

F4 = Apply (Apply FMulSym0 F2Sym0) F2Sym0 

type family F5 Source

Equations

F5 = Apply PrimeToFSym0 N5Sym0 

type family F6 Source

Equations

F6 = Apply (Apply FMulSym0 F2Sym0) F3Sym0 

type family F7 Source

Equations

F7 = Apply PrimeToFSym0 N7Sym0 

type family F8 Source

Equations

F8 = Apply (Apply FMulSym0 F2Sym0) F4Sym0 

type family F9 Source

Equations

F9 = Apply (Apply FMulSym0 F3Sym0) F3Sym0 

type family F10 Source

Equations

F10 = Apply (Apply FMulSym0 F2Sym0) F5Sym0 

type family F11 Source

Equations

F11 = Apply PrimeToFSym0 N11Sym0 

type family F12 Source

Equations

F12 = Apply (Apply FMulSym0 F4Sym0) F3Sym0 

type family F13 Source

Equations

F13 = Apply PrimeToFSym0 N13Sym0 

type family F14 Source

Equations

F14 = Apply (Apply FMulSym0 F2Sym0) F7Sym0 

type family F15 Source

Equations

F15 = Apply (Apply FMulSym0 F3Sym0) F5Sym0 

type family F16 Source

Equations

F16 = Apply (Apply FMulSym0 F2Sym0) F8Sym0 

type family F17 Source

Equations

F17 = Apply PrimeToFSym0 N17Sym0 

type family F18 Source

Equations

F18 = Apply (Apply FMulSym0 F2Sym0) F9Sym0 

type family F19 Source

Equations

F19 = Apply PrimeToFSym0 N19Sym0 

type family F20 Source

Equations

F20 = Apply (Apply FMulSym0 F2Sym0) F10Sym0 

type family F21 Source

Equations

F21 = Apply (Apply FMulSym0 F3Sym0) F7Sym0 

type family F22 Source

Equations

F22 = Apply (Apply FMulSym0 F2Sym0) F11Sym0 

type family F24 Source

Equations

F24 = Apply (Apply FMulSym0 F2Sym0) F12Sym0 

type family F25 Source

Equations

F25 = Apply (Apply FMulSym0 F5Sym0) F5Sym0 

type family F26 Source

Equations

F26 = Apply (Apply FMulSym0 F2Sym0) F13Sym0 

type family F27 Source

Equations

F27 = Apply (Apply FMulSym0 F3Sym0) F9Sym0 

type family F28 Source

Equations

F28 = Apply (Apply FMulSym0 F2Sym0) F14Sym0 

type family F30 Source

Equations

F30 = Apply (Apply FMulSym0 F2Sym0) F15Sym0 

type family F32 Source

Equations

F32 = Apply (Apply FMulSym0 F2Sym0) F16Sym0 

type family F33 Source

Equations

F33 = Apply (Apply FMulSym0 F3Sym0) F11Sym0 

type family F34 Source

Equations

F34 = Apply (Apply FMulSym0 F2Sym0) F17Sym0 

type family F35 Source

Equations

F35 = Apply (Apply FMulSym0 F5Sym0) F7Sym0 

type family F36 Source

Equations

F36 = Apply (Apply FMulSym0 F2Sym0) F18Sym0 

type family F38 Source

Equations

F38 = Apply (Apply FMulSym0 F2Sym0) F19Sym0 

type family F39 Source

Equations

F39 = Apply (Apply FMulSym0 F3Sym0) F13Sym0 

type family F40 Source

Equations

F40 = Apply (Apply FMulSym0 F2Sym0) F20Sym0 

type family F42 Source

Equations

F42 = Apply (Apply FMulSym0 F2Sym0) F21Sym0 

type family F44 Source

Equations

F44 = Apply (Apply FMulSym0 F2Sym0) F22Sym0 

type family F45 Source

Equations

F45 = Apply (Apply FMulSym0 F3Sym0) F15Sym0 

type family F48 Source

Equations

F48 = Apply (Apply FMulSym0 F2Sym0) F24Sym0 

type family F49 Source

Equations

F49 = Apply (Apply FMulSym0 F7Sym0) F7Sym0 

type family F50 Source

Equations

F50 = Apply (Apply FMulSym0 F2Sym0) F25Sym0 

type family F51 Source

Equations

F51 = Apply (Apply FMulSym0 F3Sym0) F17Sym0 

type family F52 Source

Equations

F52 = Apply (Apply FMulSym0 F2Sym0) F26Sym0 

type family F54 Source

Equations

F54 = Apply (Apply FMulSym0 F2Sym0) F27Sym0 

type family F55 Source

Equations

F55 = Apply (Apply FMulSym0 F5Sym0) F11Sym0 

type family F56 Source

Equations

F56 = Apply (Apply FMulSym0 F2Sym0) F28Sym0 

type family F57 Source

Equations

F57 = Apply (Apply FMulSym0 F3Sym0) F19Sym0 

type family F60 Source

Equations

F60 = Apply (Apply FMulSym0 F2Sym0) F30Sym0 

type family F63 Source

Equations

F63 = Apply (Apply FMulSym0 F3Sym0) F21Sym0 

type family F64 Source

Equations

F64 = Apply (Apply FMulSym0 F2Sym0) F32Sym0 

type family F65 Source

Equations

F65 = Apply (Apply FMulSym0 F5Sym0) F13Sym0 

type family F66 Source

Equations

F66 = Apply (Apply FMulSym0 F2Sym0) F33Sym0 

type family F68 Source

Equations

F68 = Apply (Apply FMulSym0 F2Sym0) F34Sym0 

type family F70 Source

Equations

F70 = Apply (Apply FMulSym0 F2Sym0) F35Sym0 

type family F72 Source

Equations

F72 = Apply (Apply FMulSym0 F2Sym0) F36Sym0 

type family F75 Source

Equations

F75 = Apply (Apply FMulSym0 F3Sym0) F25Sym0 

type family F76 Source

Equations

F76 = Apply (Apply FMulSym0 F2Sym0) F38Sym0 

type family F77 Source

Equations

F77 = Apply (Apply FMulSym0 F7Sym0) F11Sym0 

type family F78 Source

Equations

F78 = Apply (Apply FMulSym0 F2Sym0) F39Sym0 

type family F80 Source

Equations

F80 = Apply (Apply FMulSym0 F2Sym0) F40Sym0 

type family F81 Source

Equations

F81 = Apply (Apply FMulSym0 F3Sym0) F27Sym0 

type family F84 Source

Equations

F84 = Apply (Apply FMulSym0 F2Sym0) F42Sym0 

type family F85 Source

Equations

F85 = Apply (Apply FMulSym0 F5Sym0) F17Sym0 

type family F88 Source

Equations

F88 = Apply (Apply FMulSym0 F2Sym0) F44Sym0 

type family F90 Source

Equations

F90 = Apply (Apply FMulSym0 F2Sym0) F45Sym0 

type family F91 Source

Equations

F91 = Apply (Apply FMulSym0 F7Sym0) F13Sym0 

type family F95 Source

Equations

F95 = Apply (Apply FMulSym0 F5Sym0) F19Sym0 

type family F96 Source

Equations

F96 = Apply (Apply FMulSym0 F2Sym0) F48Sym0 

type family F98 Source

Equations

F98 = Apply (Apply FMulSym0 F2Sym0) F49Sym0 

type family F99 Source

Equations

F99 = Apply (Apply FMulSym0 F9Sym0) F11Sym0 

type family F128 Source

Equations

F128 = Apply (Apply FMulSym0 F2Sym0) F64Sym0 

type family F256 Source

Equations

F256 = Apply (Apply FMulSym0 F2Sym0) F128Sym0 

type family F512 Source

Equations

F512 = Apply (Apply FMulSym0 F2Sym0) F256Sym0 

type family F1024 Source

Equations

F1024 = Apply (Apply FMulSym0 F2Sym0) F512Sym0 

type family F2048 Source

Equations

F2048 = Apply (Apply FMulSym0 F2Sym0) F1024Sym0