ZkFold.Base.Algebra.Basic.Number

Documentation

class KnownNat (n :: Nat)

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0

Minimal complete definition

natSing

class KnownNat p => Prime p

Instances

Prime BLS12_381_Base

Defined in ZkFold.Base.Algebra.EllipticCurve.BLS12_381

Prime BLS12_381_Scalar

Defined in ZkFold.Base.Algebra.EllipticCurve.BLS12_381

Prime Ed25519_Base

Defined in ZkFold.Base.Algebra.EllipticCurve.Ed25519

Prime Ed25519_Scalar

Defined in ZkFold.Base.Algebra.EllipticCurve.Ed25519

(KnownNat p, KnownPrime p) => Prime p

Defined in ZkFold.Base.Algebra.Basic.Number

type family KnownPrime p where ...

Equations

KnownPrime p = If (IsPrime p) (() :: Constraint) (TypeError (NotPrimeError p))

type family IsPrime p where ...

Equations

IsPrime 0 = 'False

IsPrime 1 = 'False

IsPrime 2 = 'True

IsPrime 3 = 'True

IsPrime n = NotDividesFromTo n 2 (AtLeastSqrt n)

type family Log2 (a :: Natural) :: Natural where ...

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

value :: forall n. KnownNat n => Natural

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8

Exponentiation of type-level naturals.

Since: base-4.7.0.0