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