RosettaCodeData/Task/Pick-random-element/ACL2/pick-random-element.acl2

:set-state-ok t

(defun pick-random-element (xs state)
   (mv-let (idx state)
           (random$ (len xs) state)
      (mv (nth idx xs) state)))