    ------------------------------------------------------------------------
    -- 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 >