GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-26 14:20:59 +03:00
Code Issues Projects Releases Wiki Activity

Fix type error in examples/Karatsuba.cry.

Browse Source 
The error was caused by the recent change of the type of `demote`
when class `Literal` was introduced.
This commit is contained in:
Brian Huffman 2018-07-19 09:37:51 -07:00
parent ca1dd23173
commit b812241481
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/Karatsuba.cry
View File

@ -29,11 +29,11 @@ module Karatsuba where
kmult : {limb,n} (fin n, fin limb, limb >= 6, n >= 1) => [n] -> [n] -> [2*n]
kmult x y =
if `n >= (demote`{limb, max (width limb) (width n)}) then
if `n >= (`limb : [max (width limb) (width n)]) then
take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))
else
(zero#x)*(zero#y)
// Force a bitvector to be at least `n` bits long. As used above, this operation
// should always be a no-op, but teaches the typechecker a necessary inequality