ZkFold.Base.Algebra.Basic.Number

Documentation

data Natural

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Instances

FromJSON Natural

Defined in Data.Aeson.Types.FromJSON

Methods

parseJSON :: Value -> Parser Natural

parseJSONList :: Value -> Parser [Natural]

FromJSONKey Natural

Defined in Data.Aeson.Types.FromJSON

Methods

fromJSONKey :: FromJSONKeyFunction Natural

fromJSONKeyList :: FromJSONKeyFunction [Natural]

ToJSON Natural

Defined in Data.Aeson.Types.ToJSON

Methods

toJSON :: Natural -> Value

toEncoding :: Natural -> Encoding

toJSONList :: [Natural] -> Value

toEncodingList :: [Natural] -> Encoding

ToJSONKey Natural

Defined in Data.Aeson.Types.ToJSON

Methods

toJSONKey :: ToJSONKeyFunction Natural

toJSONKeyList :: ToJSONKeyFunction [Natural]

Data Natural

Since: base-4.8.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural

toConstr :: Natural -> Constr

dataTypeOf :: Natural -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural)

gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

Bits Natural

Since: base-4.8.0

Defined in GHC.Bits

Methods

(.&.) :: Natural -> Natural -> Natural

(.|.) :: Natural -> Natural -> Natural

xor :: Natural -> Natural -> Natural

complement :: Natural -> Natural

shift :: Natural -> Int -> Natural

rotate :: Natural -> Int -> Natural

zeroBits :: Natural

bit :: Int -> Natural

setBit :: Natural -> Int -> Natural

clearBit :: Natural -> Int -> Natural

complementBit :: Natural -> Int -> Natural

testBit :: Natural -> Int -> Bool

bitSizeMaybe :: Natural -> Maybe Int

bitSize :: Natural -> Int

isSigned :: Natural -> Bool

shiftL :: Natural -> Int -> Natural

unsafeShiftL :: Natural -> Int -> Natural

shiftR :: Natural -> Int -> Natural

unsafeShiftR :: Natural -> Int -> Natural

rotateL :: Natural -> Int -> Natural

rotateR :: Natural -> Int -> Natural

popCount :: Natural -> Int

Enum Natural

Since: base-4.8.0.0

Defined in GHC.Enum

Methods

succ :: Natural -> Natural

pred :: Natural -> Natural

toEnum :: Int -> Natural

fromEnum :: Natural -> Int

enumFrom :: Natural -> [Natural]

enumFromThen :: Natural -> Natural -> [Natural]

enumFromTo :: Natural -> Natural -> [Natural]

enumFromThenTo :: Natural -> Natural -> Natural -> [Natural]

Num Natural

Note that Natural's Num instance isn't a ring: no element but 0 has an additive inverse. It is a semiring though.

Since: base-4.8.0.0

Defined in GHC.Num

Methods

(+) :: Natural -> Natural -> Natural

(-) :: Natural -> Natural -> Natural

(*) :: Natural -> Natural -> Natural

negate :: Natural -> Natural

abs :: Natural -> Natural

signum :: Natural -> Natural

fromInteger :: Integer -> Natural

Read Natural

Since: base-4.8.0.0

Defined in GHC.Read

Methods

readsPrec :: Int -> ReadS Natural

readList :: ReadS [Natural]

readPrec :: ReadPrec Natural

readListPrec :: ReadPrec [Natural]

Integral Natural

Since: base-4.8.0.0

Defined in GHC.Real

Methods

quot :: Natural -> Natural -> Natural

rem :: Natural -> Natural -> Natural

div :: Natural -> Natural -> Natural

mod :: Natural -> Natural -> Natural

quotRem :: Natural -> Natural -> (Natural, Natural)

divMod :: Natural -> Natural -> (Natural, Natural)

toInteger :: Natural -> Integer

Real Natural

Since: base-4.8.0.0

Defined in GHC.Real

Methods

toRational :: Natural -> Rational

Show Natural

Since: base-4.8.0.0

Defined in GHC.Show

Methods

showsPrec :: Int -> Natural -> ShowS

show :: Natural -> String

showList :: [Natural] -> ShowS

Binary Natural

Since: binary-0.7.3.0

Defined in Data.Binary.Class

Methods

put :: Natural -> Put

get :: Get Natural

putList :: [Natural] -> Put

NFData Natural

Since: deepseq-1.4.0.0

Defined in Control.DeepSeq

Methods

rnf :: Natural -> ()

Eq Natural

Defined in GHC.Num.Natural

Methods

(==) :: Natural -> Natural -> Bool

(/=) :: Natural -> Natural -> Bool

Ord Natural

Defined in GHC.Num.Natural

Methods

compare :: Natural -> Natural -> Ordering

(<) :: Natural -> Natural -> Bool

(<=) :: Natural -> Natural -> Bool

(>) :: Natural -> Natural -> Bool

(>=) :: Natural -> Natural -> Bool

max :: Natural -> Natural -> Natural

min :: Natural -> Natural -> Natural

Hashable Natural

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> Natural -> Int

hash :: Natural -> Int

Pretty Natural

Defined in Prettyprinter.Internal

Methods

pretty :: Natural -> Doc ann

prettyList :: [Natural] -> Doc ann

UniformRange Natural

Defined in System.Random.Internal

Methods

uniformRM :: StatefulGen g m => (Natural, Natural) -> g -> m Natural

ToParamSchema Natural

Defined in Data.Swagger.Internal.ParamSchema

Methods

toParamSchema :: forall (t :: SwaggerKind Type). Proxy Natural -> ParamSchema t

ToSchema Natural

Defined in Data.Swagger.Internal.Schema

Methods

declareNamedSchema :: Proxy Natural -> Declare (Definitions Schema) NamedSchema

AdditiveMonoid Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

zero :: Natural

AdditiveSemigroup Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(+) :: Natural -> Natural -> Natural

BinaryExpansion Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Associated Types

type Bits Natural

Methods

binaryExpansion :: Natural -> Bits Natural

fromBinary :: Bits Natural -> Natural

MultiplicativeMonoid Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

one :: Natural

MultiplicativeSemigroup Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(*) :: Natural -> Natural -> Natural

SemiEuclidean Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

divMod :: Natural -> Natural -> (Natural, Natural)

div :: Natural -> Natural -> Natural

mod :: Natural -> Natural -> Natural

Semiring Natural

Defined in ZkFold.Base.Algebra.Basic.Class

TestCoercion SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b)

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

Exponent Rational Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(^) :: Rational -> Natural -> Rational

Exponent BLS12_381_GT Natural

Defined in ZkFold.Base.Algebra.EllipticCurve.BLS12_381

Methods

(^) :: BLS12_381_GT -> Natural -> BLS12_381_GT

Exponent BN254_GT Natural

Defined in ZkFold.Base.Algebra.EllipticCurve.BN254

Methods

(^) :: BN254_GT -> Natural -> BN254_GT

Exponent Integer Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(^) :: Integer -> Natural -> Integer

Exponent Natural Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(^) :: Natural -> Natural -> Natural

FromConstant Natural Rational

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

fromConstant :: Natural -> Rational

FromConstant Natural Integer

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

fromConstant :: Natural -> Integer

FromConstant Natural Bool

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

fromConstant :: Natural -> Bool

Scale Natural Rational

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

scale :: Natural -> Rational -> Rational

Scale Natural Integer

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

scale :: Natural -> Integer -> Integer

Scale Natural Bool

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

scale :: Natural -> Bool -> Bool

Eq Bool Natural

Defined in ZkFold.Symbolic.Data.Eq

Methods

(==) :: Natural -> Natural -> Bool

(/=) :: Natural -> Natural -> Bool

Lift Natural

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Quote m => Natural -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Natural -> Code m Natural

KnownNat n => Reifies (n :: Nat) Integer

Defined in Data.Reflection

Methods

reflect :: proxy n -> Integer

() :=> (Bits Natural)

Defined in Data.Constraint

Methods

ins :: () :- Bits Natural

() :=> (Enum Natural)

Defined in Data.Constraint

Methods

ins :: () :- Enum Natural

() :=> (Num Natural)

Defined in Data.Constraint

Methods

ins :: () :- Num Natural

() :=> (Read Natural)

Defined in Data.Constraint

Methods

ins :: () :- Read Natural

() :=> (Integral Natural)

Defined in Data.Constraint

Methods

ins :: () :- Integral Natural

() :=> (Real Natural)

Defined in Data.Constraint

Methods

ins :: () :- Real Natural

() :=> (Show Natural)

Defined in Data.Constraint

Methods

ins :: () :- Show Natural

() :=> (Eq Natural)

Defined in Data.Constraint

Methods

ins :: () :- Eq Natural

() :=> (Ord Natural)

Defined in Data.Constraint

Methods

ins :: () :- Ord Natural

KnownNat p => FromConstant Natural (Zp p)

Defined in ZkFold.Base.Algebra.Basic.Field

Methods

fromConstant :: Natural -> Zp p

FromConstant Natural (UInt 11 'Auto c) => FromConstant Natural (UTCTime c)

Defined in ZkFold.Symbolic.Data.UTCTime

Methods

fromConstant :: Natural -> UTCTime c

FromConstant Natural a => FromConstant Natural (Maybe a)

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

fromConstant :: Natural -> Maybe a

KnownNat p => Scale Natural (Zp p)

Defined in ZkFold.Base.Algebra.Basic.Field

Methods

scale :: Natural -> Zp p -> Zp p

EllipticCurve curve => Scale Natural (Point curve)

Defined in ZkFold.Base.Algebra.EllipticCurve.Class

Methods

scale :: Natural -> Point curve -> Point curve

Scale Natural a => Scale Natural (Maybe a)

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

scale :: Natural -> Maybe a -> Maybe a

(FromConstant Natural c, AdditiveMonoid c, KnownNat size) => FromConstant Natural (PolyVec c size)

Defined in ZkFold.Base.Algebra.Polynomials.Univariate

Methods

fromConstant :: Natural -> PolyVec c size

FromConstant Natural (EuclideanF a v)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

fromConstant :: Natural -> EuclideanF a v

FromConstant Natural (WitnessF a v)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

fromConstant :: Natural -> WitnessF a v

FromConstant Natural a => FromConstant Natural (UVar a i)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation

Methods

fromConstant :: Natural -> UVar a i

(Symbolic c, KnownNat n) => FromConstant Natural (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: Natural -> ByteString n c

Scale Natural (EuclideanF a v)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

scale :: Natural -> EuclideanF a v -> EuclideanF a v

Scale Natural (WitnessF a v)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

scale :: Natural -> WitnessF a v -> WitnessF a v

(Semiring a, Eq a) => Scale Natural (UVar a i)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation

Methods

scale :: Natural -> UVar a i -> UVar a i

(Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

fromConstant :: Natural -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Natural (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

scale :: Natural -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: Natural -> UInt n rs c

AdditiveGroup (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Methods

(-) :: MerkleHash ('Just n) -> MerkleHash ('Just n) -> MerkleHash ('Just n)

negate :: MerkleHash ('Just n) -> MerkleHash ('Just n)

Field (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Methods

(//) :: MerkleHash ('Just n) -> MerkleHash ('Just n) -> MerkleHash ('Just n)

finv :: MerkleHash ('Just n) -> MerkleHash ('Just n)

rootOfUnity :: Natural -> Maybe (MerkleHash ('Just n))

Finite (Zp n) => Finite (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Associated Types

type Order (MerkleHash ('Just n)) :: Natural

Ring (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

SemiEuclidean (MerkleHash ('Nothing :: Maybe Natural))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Methods

divMod :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> (MerkleHash 'Nothing, MerkleHash 'Nothing)

div :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> MerkleHash 'Nothing

mod :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> MerkleHash 'Nothing

SemiEuclidean Natural => SemiEuclidean (Maybe Natural)

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

divMod :: Maybe Natural -> Maybe Natural -> (Maybe Natural, Maybe Natural)

div :: Maybe Natural -> Maybe Natural -> Maybe Natural

mod :: Maybe Natural -> Maybe Natural -> Maybe Natural

ToConstant (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Associated Types

type Const (MerkleHash ('Just n))

Methods

toConstant :: MerkleHash ('Just n) -> Const (MerkleHash ('Just n))

KnownNat p => Exponent (Zp p) Natural

Defined in ZkFold.Base.Algebra.Basic.Field

Methods

(^) :: Zp p -> Natural -> Zp p

(Field c, Eq c) => Exponent (Poly c) Natural

Defined in ZkFold.Base.Algebra.Polynomials.Univariate

Methods

(^) :: Poly c -> Natural -> Poly c

Exponent (MerkleHash n) Natural

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

Methods

(^) :: MerkleHash n -> Natural -> MerkleHash n

Symbolic c => Exponent (FieldElement c) Natural

Defined in ZkFold.Symbolic.Data.FieldElement

Methods

(^) :: FieldElement c -> Natural -> FieldElement c

Exponent a Natural => Exponent (Maybe a) Natural

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

(^) :: Maybe a -> Natural -> Maybe a

FromConstant Natural a => FromConstant (Maybe Natural) (Maybe a)

Defined in ZkFold.Base.Algebra.Basic.Class

Methods

fromConstant :: Maybe Natural -> Maybe a

FromConstant Natural a => FromConstant (Maybe Natural) (UVar a i)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation

Methods

fromConstant :: Maybe Natural -> UVar a i

MultiplicativeMonoid (Ext2 f e) => Exponent (Ext2 f e) Natural

Defined in ZkFold.Base.Algebra.Basic.Field

Methods

(^) :: Ext2 f e -> Natural -> Ext2 f e

MultiplicativeMonoid (Ext3 f e) => Exponent (Ext3 f e) Natural

Defined in ZkFold.Base.Algebra.Basic.Field

Methods

(^) :: Ext3 f e -> Natural -> Ext3 f e

Monomial i j => Exponent (Mono i j) Natural

Defined in ZkFold.Base.Algebra.Polynomials.Multivariate.Monomial

Methods

(^) :: Mono i j -> Natural -> Mono i j

(Field c, KnownNat size) => Exponent (PolyVec c size) Natural

Defined in ZkFold.Base.Algebra.Polynomials.Univariate

Methods

(^) :: PolyVec c size -> Natural -> PolyVec c size

Exponent (EuclideanF a v) Natural

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

(^) :: EuclideanF a v -> Natural -> EuclideanF a v

Exponent (WitnessF a v) Natural

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness

Methods

(^) :: WitnessF a v -> Natural -> WitnessF a v

MultiplicativeMonoid a => Exponent (UVar a i) Natural

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation

Methods

(^) :: UVar a i -> Natural -> UVar a i

(KnownNat p, Symbolic c) => Exponent (FFA p c) Natural

Defined in ZkFold.Symbolic.Data.FFA

Methods

(^) :: FFA p c -> Natural -> FFA p c

(path ~ GPositionPath con epath, When (IsLeft epath) (HideReps g h), GFieldProd path g h a b) => GPositionSum ('PathLeaf epath) (M1 C ('MetaCons con fix hs) g) (M1 C ('MetaCons con fix hs) h) a b

Defined in Optics.Internal.Generic

Methods

gpositionSum :: LensVL (M1 C ('MetaCons con fix hs) g x) (M1 C ('MetaCons con fix hs) h x) a b

Polynomial c i j => Exponent (Poly c i j) Natural

Defined in ZkFold.Base.Algebra.Polynomials.Multivariate.Polynomial

Methods

(^) :: Poly c i j -> Natural -> Poly c i j

MultiplicativeMonoid (UInt n r c) => Exponent (UInt n r c) Natural

Defined in ZkFold.Symbolic.Data.UInt

Methods

(^) :: UInt n r c -> Natural -> UInt n r c

(GPositionSum path1 g1 h1 a b, GPositionSum path2 g2 h2 a b) => GPositionSum ('PathTree path1 path2) (g1 :+: g2) (h1 :+: h2) a b

Defined in Optics.Internal.Generic

Methods

gpositionSum :: LensVL ((g1 :+: g2) x) ((h1 :+: h2) x) a b

type Bits Natural

Defined in ZkFold.Base.Algebra.Basic.Class

type Bits Natural = [Natural]

type Compare (a :: Natural) (b :: Natural)

Defined in Data.Type.Ord

type Compare (a :: Natural) (b :: Natural) = CmpNat a b

type Eval (Sum ns :: Nat -> Type)

Defined in Fcf.Class.Foldable

type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

type Eval (Length ('[] :: [a]) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length ('[] :: [a]) :: Nat -> Type) = 0

type Eval (Length (a2 ': as) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)

type Eval (a * b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a * b :: Nat -> Type) = a * b

type Eval (a + b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a + b :: Nat -> Type) = a + b

type Eval (a - b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a - b :: Nat -> Type) = a - b

type Eval (a ^ b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b

type Const (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

type Const (MerkleHash ('Just n)) = MerkleHash ('Nothing :: Maybe Natural)

type Order (MerkleHash ('Just n))

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash

type Order (MerkleHash ('Just n)) = n

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) = 'Nothing :: Maybe Nat

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure ('Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))

type Eval (NumIter a s :: Maybe (k, Nat) -> Type)

Defined in Fcf.Data.List

type Eval (NumIter a s :: Maybe (k, Nat) -> Type) = If (Eval (s > 0)) ('Just '(a, s - 1)) ('Nothing :: Maybe (k, Natural))

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 BN254_Base

Defined in ZkFold.Base.Algebra.EllipticCurve.BN254

Prime BN254_Scalar

Defined in ZkFold.Base.Algebra.EllipticCurve.BN254

Prime Ed25519_Base

Defined in ZkFold.Base.Algebra.EllipticCurve.Ed25519

Prime Ed25519_Scalar

Defined in ZkFold.Base.Algebra.EllipticCurve.Ed25519

Prime FpModulus

Defined in ZkFold.Base.Algebra.EllipticCurve.Pasta

Prime FqModulus

Defined in ZkFold.Base.Algebra.EllipticCurve.Pasta

Prime Secp256k1_Base

Defined in ZkFold.Base.Algebra.EllipticCurve.Secp256k1

Prime Secp256k1_Scalar

Defined in ZkFold.Base.Algebra.EllipticCurve.Secp256k1

(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

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

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

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

Division (round down) of natural numbers. Div x 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