Modulecardano-crypto-1.3.0Haskell2010

Crypto.Math.NatMath

familytype family Div8 (bitLen :: Nat) :: Nat where

familytype family IsDiv8 (bitLen :: Nat) (n :: Nat) :: Bool where

IsDiv8 bitLen 0 = 'True
IsDiv8 bitLen 1 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 2 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 3 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 4 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 5 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 6 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen 7 = TypeError (('Text "bitLen " ':<>: 'ShowType bitLen) ':<>: 'Text " is not divisible by 8")
IsDiv8 bitLen n = IsDiv8 n (Mod8 n)

familytype family Mod8 (n :: Nat) :: Natural where

typetype IsDivisibleBy8 (bitLen :: Nat) = IsDiv8 bitLen bitLen ~ 'True