		Search-engine friendly clone of the ACL2 documentation.

Aig-random-sim

N-random-60-bit-nats

Generate a list of 60-bit naturals.

Signature
(n-random-60-bit-nats n state) → (mv * state)
Arguments: n — How many to generate.
Guard (natp n).

We just leave this enabled.

Definitions and Theorems

Function: n-random-60-bit-nats

(defun n-random-60-bit-nats (n state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'n-random-60-bit-nats))
    (declare (ignorable __function__))
    (random-list n (ash 1 60) state)))