diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-20 00:08:08 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-20 00:08:20 -0400 |
| commit | a2e8a332f4ea13d90d56e00fdc8419d8ba245e5c (patch) | |
| tree | a186ec3c44cc6a5b6c5458ba6add704bb0b445b5 /src/Arithmetic | |
| parent | 774f4b57cc000880f9ce31da4eb71d7f4c10317e (diff) | |
Use div_cps, modulo_cps
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v index 2118fcdfc..fa7bbe919 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -166,7 +166,9 @@ Module Columns. Fixpoint compact_digit_cps (digit : list Z) (f:Z * Z->T) := match digit with | nil => f (0, 0) - | x :: nil => f (div x (weight (S n) / weight n), modulo x (weight (S n) / weight n)) + | x :: nil => div_cps x (weight (S n) / weight n) (fun d => + modulo_cps x (weight (S n) / weight n) (fun m => + f (d, m))) | x :: y :: nil => add_get_carry_cps _ (weight (S n) / weight n) x y (fun sum_carry => dlet sum_carry := sum_carry in |