------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe operations over linear congruential pseudo random generators
-- for natural numbers
-- /!\ NB: LCGs must not be used for cryptographic applications
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
open import Codata.Sized.Stream using (Stream; unfold)
open import Data.Nat.PseudoRandom.LCG using (Generator; step)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (<_,_>)
open import Function.Base using (id)
module Data.Nat.PseudoRandom.LCG.Unsafe where
------------------------------------------------------------------------
-- An infinite stream of random numbers
stream : Generator → ℕ → Stream ℕ _
stream gen = unfold < step gen , id >
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4