GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Fix constraints on type of primitive intmod.

Browse Source 
The old type did not forbid literals of the invalid type `Z inf`.
This commit is contained in:
Brian Huffman 2018-06-14 12:24:32 -07:00
parent 59104829a0
commit dda5d34131
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Cryptol.cry
View File

@ -18,7 +18,7 @@ primitive integer : {val} (fin val) => Integer
/**
* The integer (mod n) value corresponding to a numeric type.
*/
primitive intmod : {val, modulus} (fin val, modulus >= val + 1) => Z modulus
primitive intmod : {val, modulus} (fin modulus, modulus >= val + 1) => Z modulus
infixr 5 ==>
infixr 10 \/

3
tests/issues/issue226.icry.stdout
View File

@ -89,7 +89,8 @@ Symbols
infFrom : {bits} (fin bits) => [bits] -> [inf][bits]
infFromThen : {bits} (fin bits) => [bits] -> [bits] -> [inf][bits]
integer : {val} (fin val) => Integer
intmod : {val, modulus} (fin val, modulus >= 1 + val) => Z modulus
intmod :
{val, modulus} (fin modulus, modulus >= 1 + val) => Z modulus
iterate : {a} (a -> a) -> a -> [inf]a
join :
{parts, each, a} (fin each) => [parts][each]a -> [parts * each]a