diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-31 11:37:09 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-31 11:39:09 -0400 |
| commit | 245e628bdf827d1ff4e217a84603ee91da07ed1c (patch) | |
| tree | f6764f5a8154662c6c4bda4c3861b6063dd4b9fc /src | |
| parent | 45d8ed0e66d6b456d7d6e8cd299e5a1ff94cae41 (diff) | |
Fix a typo making word calculations wrong
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Interpretations.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 413fcf5cf..46931d2e2 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -57,9 +57,9 @@ Module Word64. Definition sub : word64 -> word64 -> word64 := @wminus _. Definition mul : word64 -> word64 -> word64 := @wmult _. Definition shl : word64 -> word64 -> word64 - := fun x y => NToWord _ (Z.to_N (Z.shiftl (Z.of_N (wordToN x)) (Z.of_N (wordToN x)))). + := fun x y => NToWord _ (N.shiftl (wordToN x) (wordToN y)). Definition shr : word64 -> word64 -> word64 - := fun x y => NToWord _ (Z.to_N (Z.shiftr (Z.of_N (wordToN x)) (Z.of_N (wordToN x)))). + := fun x y => NToWord _ (N.shiftr (wordToN x) (wordToN y)). Definition land : word64 -> word64 -> word64 := @wand _. Definition lor : word64 -> word64 -> word64 := @wor _. Definition neg : word64 -> word64 -> word64 (* TODO: FIXME? *) |