cryptol/tests/issues/issue130.cry
2014-10-23 15:00:34 -07:00

11 lines
227 B
Plaintext

parity xs = ys!0
where ys = [False] # [y ^ x | x <- xs | y <- ys ]
foldl1 f xs = ys!0
where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ]
par = foldl1 (^)
parOK : {n} [n+1] -> Bit
property parOK x = par x == parity x