diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-22 14:25:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-22 14:58:53 -0400 |
| commit | f7e7c340ab08de79db745db5d2b699dd99dc407a (patch) | |
| tree | a51dfdf846280e6ef441d0859662d5b40d3e8a99 /src/BoundedArithmetic/DoubleBounded.v | |
| parent | 8ee7882b46d4b8aba92fed51391d03ae8d418a43 (diff) | |
Use dlet, not llet
Diffstat (limited to 'src/BoundedArithmetic/DoubleBounded.v')
| -rw-r--r-- | src/BoundedArithmetic/DoubleBounded.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/BoundedArithmetic/DoubleBounded.v b/src/BoundedArithmetic/DoubleBounded.v index b6aa858ff..5cf48cd3b 100644 --- a/src/BoundedArithmetic/DoubleBounded.v +++ b/src/BoundedArithmetic/DoubleBounded.v @@ -6,7 +6,7 @@ Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LockedLet. +Require Import Crypto.Util.LetIn. Local Open Scope nat_scope. Local Open Scope Z_scope. @@ -28,13 +28,13 @@ Section ripple_carry_definitions. : forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k := match k return forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k with | O => f - | S k' => fun xss yss carry => llet xss := xss in - llet yss := yss in + | S k' => fun xss yss carry => dlet xss := xss in + dlet yss := yss in let '(xs, x) := eta xss in let '(ys, y) := eta yss in - llet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in + dlet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in let '(carry, zs) := eta addv in - llet fxy := (f x y carry) in + dlet fxy := (f x y carry) in let '(carry, z) := eta fxy in (carry, (zs, z)) end. @@ -80,15 +80,15 @@ Section tuple2. {ldi : load_immediate W}. Definition mul_double (a b : W) : tuple W 2 - := llet a := a in - llet b := b in + := dlet a := a in + dlet b := b in let out : tuple W 2 := (mulhwll a b, mulhwhh a b) in - llet out := out in - llet tmp := mulhwhl a b in - llet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in + dlet out := out in + dlet tmp := mulhwhl a b in + dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in let '(_, out) := eta addv in - llet tmp := mulhwhl b a in - llet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in + dlet tmp := mulhwhl b a in + dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in let '(_, out) := eta addv in out. |