Cryptol implementation of LCG

lcg : {n,b} (fin n) => [b] -> [b] -> [b/2] -> [b] -> [n][b/2]
lcg seed inc ex mult = [rand | (_,rand) <- take`{n} (drop`{1} seq) ]
  where
    succ st = st * mult + inc
    out  st = (take`{b/2} (st * mult + inc)) ^ ex
    seq = [(seed,0)] # [(succ st, out st) | (st,_) <- seq]