### RANDOM$

obtain a random value
Major Section: ACL2-BUILT-INS

Example:
(random$ 10 state) ==> (mv 7 <state>)

`(Random$ limit state)`

, where `limit`

is a positive integer, returns a
random non-negative integer together with a new `state`

. Logically, it
simply returns the first element of a list that is a field of the ACL2
`state`

, called the `acl2-oracle`

, together with the new state
resulting from removing that element from that list. (Except, if that
element is not in range as specified above, then 0 is returned.) However,
`random$`

actually invokes a Common Lisp function to choose the integer
returned. Quoting from the Common Lisp HyperSpec(TM),
http://www.lispworks.com/documentation/HyperSpec/Front:
``An approximately uniform choice distribution is used... each of the
possible results occurs with (approximate) probability 1/limit.''

Consider enabling rules `natp-random$`

and `random$-linear`

if you want
to reason about `random$`

.