Crypto.Random

Definitions

interface DRG : Type -> Type

Parameters: a
Methods:

next_bytes : (n : Nat) -> a -> (a, Vect n Bits8)

Implementation: 

DRG ChaCha12DRG

next_bytes : DRG a => (n : Nat) -> a -> (a, Vect n Bits8)

Visibility: public export

interface MonadRandom : (Type -> Type) -> Type

Parameters: m
Constraints: Monad m
Methods:

random_bytes : (n : Nat) -> m (Vect n Bits8)

Implementation: 

DRG s => MonadRandom (State s)

random_bytes : MonadRandom m => (n : Nat) -> m (Vect n Bits8)

Visibility: public export

next_integer : MonadRandom m => Nat -> m Integer

Visibility: public export

uniform_random : MonadRandom m => Integer -> m Integer

Visibility: public export

uniform_random' : MonadRandom m => Integer -> Integer -> m Integer

Visibility: public export

data ChaCha12DRG : Type

Totality: total
Visibility: public export
Constructor: 

MkChaCha12DRG : Vect 8 Bits32 -> ChaCha12DRG

Hint: 

DRG ChaCha12DRG

new_chacha12_drg : MonadRandom m => m ChaCha12DRG

Visibility: public export