diff options
Diffstat (limited to 'src/ModularArithmetic/Pow2Base.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2Base.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index a2c76016d..9d6cc2410 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -53,14 +53,19 @@ Section Pow2Base. (Z.pow2_mod di (log_cap i), Z.shiftr di (log_cap i)). + (* [fi] is fed [length us] and [S i] and produces the index of + the digit to which value should be added; + [fc] modifies the carried value before adding it to that digit *) Definition carry_gen fc fi i := fun us => - let i := fi (length us) i in + let i := fi i in let di := nth_default 0 us i in let '(di', ci) := carry_single i di in let us' := set_nth i di' us in - add_to_nth (fi (length us) (S i)) (fc ci) us'. + add_to_nth (fi (S i)) (fc ci) us'. - Definition carry_simple := carry_gen (fun ci => ci) (fun _ i => i). + (* carry_simple does not modify the carried value, and always adds it + to the digit with index [S i] *) + Definition carry_simple := carry_gen (fun ci => ci) (fun i => i). Definition carry_simple_sequence is us := fold_right carry_simple us is. |