		Search-engine friendly clone of the ACL2 documentation.

Random-list

Generate a list of random numbers in [0, limit).

Function: random-list

(defun random-list (n limit state)
  (declare (xargs :guard (and (natp n) (posp limit))))
  (random-list-aux n limit nil state))

Theorem: nat-listp-of-random-list

(defthm nat-listp-of-random-list
  (nat-listp (mv-nth 0 (random-list n limit state))))

Theorem: state-p1-of-random-list

(defthm state-p1-of-random-list
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1 (random-list n limit state)))))