idris-lang/Idris-dev — pull request #1119 by KesterTong (2014-04-28 18:54:59+00:00)
Title: Fix/master/random

This pull request modifies the Effect/Random package. It changes the definition of rndFin, and adds two functions to select random elements from vectors and lists. It also adds docstrings to some functions in that package.