Basement.Bounded

Types to represent ℤ/nℤ.

ℤ/nℤ is a finite field and is defined as the set of natural number: {0, 1, ..., n − 1}.

Documentation

data Zn64 (n :: Nat)

A type level bounded natural backed by a Word64

Instances

Eq (Zn64 n)

Methods

(==) :: Zn64 n -> Zn64 n -> Bool

(/=) :: Zn64 n -> Zn64 n -> Bool

(KnownNat n, NatWithinBound Word64 n) => Num (Zn64 n)

Methods

(+) :: Zn64 n -> Zn64 n -> Zn64 n

(-) :: Zn64 n -> Zn64 n -> Zn64 n

(*) :: Zn64 n -> Zn64 n -> Zn64 n

negate :: Zn64 n -> Zn64 n

abs :: Zn64 n -> Zn64 n

signum :: Zn64 n -> Zn64 n

fromInteger :: Integer -> Zn64 n

Ord (Zn64 n)

Methods

compare :: Zn64 n -> Zn64 n -> Ordering

(<) :: Zn64 n -> Zn64 n -> Bool

(<=) :: Zn64 n -> Zn64 n -> Bool

(>) :: Zn64 n -> Zn64 n -> Bool

(>=) :: Zn64 n -> Zn64 n -> Bool

max :: Zn64 n -> Zn64 n -> Zn64 n

min :: Zn64 n -> Zn64 n -> Zn64 n

Show (Zn64 n)

Methods

showsPrec :: Int -> Zn64 n -> ShowS

show :: Zn64 n -> String

showList :: [Zn64 n] -> ShowS

(KnownNat n, NatWithinBound Word64 n) => Subtractive (Zn64 n)

Associated Types

type Difference (Zn64 n) :: *

Methods

(-) :: Zn64 n -> Zn64 n -> Difference (Zn64 n)

(KnownNat n, NatWithinBound Word64 n) => Additive (Zn64 n)

Methods

azero :: Zn64 n

(+) :: Zn64 n -> Zn64 n -> Zn64 n

scale :: IsNatural n => n -> Zn64 n -> Zn64 n

NormalForm (Zn64 n)

Methods

toNormalForm :: Zn64 n -> ()

From (Zn64 n) Word256

Methods

from :: Zn64 n -> Word256

From (Zn64 n) Word128

Methods

from :: Zn64 n -> Word128

From (Zn64 n) Word64

Methods

from :: Zn64 n -> Word64

(KnownNat n, NatWithinBound Word32 n) => From (Zn64 n) Word32

Methods

from :: Zn64 n -> Word32

(KnownNat n, NatWithinBound Word16 n) => From (Zn64 n) Word16

Methods

from :: Zn64 n -> Word16

(KnownNat n, NatWithinBound Word8 n) => From (Zn64 n) Word8

Methods

from :: Zn64 n -> Word8

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n)

Methods

from :: Zn n -> Zn64 n

KnownNat n => From (Zn64 n) (Zn n)

Methods

from :: Zn64 n -> Zn n

type Difference (Zn64 n)

type Difference (Zn64 n) = Zn64 n

unZn64 :: Zn64 n -> Word64

data Zn (n :: Nat)

A type level bounded natural

Instances

Eq (Zn n)

Methods

(==) :: Zn n -> Zn n -> Bool

(/=) :: Zn n -> Zn n -> Bool

KnownNat n => Num (Zn n)

Methods

(+) :: Zn n -> Zn n -> Zn n

(-) :: Zn n -> Zn n -> Zn n

(*) :: Zn n -> Zn n -> Zn n

negate :: Zn n -> Zn n

abs :: Zn n -> Zn n

signum :: Zn n -> Zn n

fromInteger :: Integer -> Zn n

Ord (Zn n)

Methods

compare :: Zn n -> Zn n -> Ordering

(<) :: Zn n -> Zn n -> Bool

(<=) :: Zn n -> Zn n -> Bool

(>) :: Zn n -> Zn n -> Bool

(>=) :: Zn n -> Zn n -> Bool

max :: Zn n -> Zn n -> Zn n

min :: Zn n -> Zn n -> Zn n

Show (Zn n)

Methods

showsPrec :: Int -> Zn n -> ShowS

show :: Zn n -> String

showList :: [Zn n] -> ShowS

KnownNat n => Subtractive (Zn n)

Associated Types

type Difference (Zn n) :: *

Methods

(-) :: Zn n -> Zn n -> Difference (Zn n)

KnownNat n => Additive (Zn n)

Methods

azero :: Zn n

(+) :: Zn n -> Zn n -> Zn n

scale :: IsNatural n => n -> Zn n -> Zn n

NormalForm (Zn n)

Methods

toNormalForm :: Zn n -> ()

(KnownNat n, NatWithinBound Word256 n) => From (Zn n) Word256

Methods

from :: Zn n -> Word256

(KnownNat n, NatWithinBound Word128 n) => From (Zn n) Word128

Methods

from :: Zn n -> Word128

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) Word64

Methods

from :: Zn n -> Word64

(KnownNat n, NatWithinBound Word32 n) => From (Zn n) Word32

Methods

from :: Zn n -> Word32

(KnownNat n, NatWithinBound Word16 n) => From (Zn n) Word16

Methods

from :: Zn n -> Word16

(KnownNat n, NatWithinBound Word8 n) => From (Zn n) Word8

Methods

from :: Zn n -> Word8

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n)

Methods

from :: Zn n -> Zn64 n

KnownNat n => From (Zn64 n) (Zn n)

Methods

from :: Zn64 n -> Zn n

type Difference (Zn n)

type Difference (Zn n) = Zn n

unZn :: Zn n -> Natural

zn64 :: forall n. (KnownNat n, NatWithinBound Word64 n) => Word64 -> Zn64 n

Create an element of ℤ/nℤ from a Word64

If the value is greater than n, then the value is normalized by using the integer modulus n

zn :: forall n. KnownNat n => Natural -> Zn n

Create an element of ℤ/nℤ from a Natural.

If the value is greater than n, then the value is normalized by using the integer modulus n

zn64Nat :: forall m n. (KnownNat m, KnownNat n, NatWithinBound Word64 m, NatWithinBound Word64 n, CmpNat m n ~ LT) => Proxy m -> Zn64 n

Create an element of ℤ/nℤ from a type level Nat

znNat :: forall m n. (KnownNat m, KnownNat n, CmpNat m n ~ LT) => Proxy m -> Zn n

Create an element of ℤ/nℤ from a type level Nat