GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 23:17:42 +03:00
Code Issues Projects Releases Wiki Activity

Add function generate to Cryptol prelude.

Browse Source 
generate : {n, ix, a}
  (fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]
This commit is contained in:
Brian Huffman 2019-06-18 15:39:13 -07:00
parent ec7c9a0f6e
commit 2df66aa7c1
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
lib/Cryptol.cry
View File

@ -492,6 +492,14 @@ primitive infFrom : {a} (Arith a) => a -> [inf]a
*/
primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a
/**
* Produce a sequence using a generating function.
* Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.
*/
generate : {n, ix, a}
(fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]
primitive error : {a, len} (fin len) => [len][8] -> a