diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-07-19 18:25:20 +0200 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-07-19 18:25:20 +0200 |
| commit | 51602bd1ccf7493e53f78afa958238cad14571f2 (patch) | |
| tree | 1a51ab17bd53dd51f9e983e48cb792d0eee1336c /src/ModularArithmetic | |
| parent | 34246fa38df7b039f046d3851e923283dd07896a (diff) | |
Use update_nth in add_to_nth (#26)
It leads to a slightly more transparent and clearer definition.
If I got everything right, nothing should depend on the judgmental
definition of [add_to_nth] anymore.
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2Base.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index b842fa713..acc96ad73 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -48,14 +48,8 @@ Section Pow2Base. carrying. *) Notation log_cap i := (nth_default 0 limb_widths i). - - Definition add_to_nth n (x:Z) xs := - set_nth n (x + nth_default 0 xs n) xs. - (* TODO: Maybe we should use this instead? *) - (* Definition add_to_nth n (x:Z) xs := update_nth n (fun y => x + y) xs. - *) Definition carry_and_reduce_single i := fun di => (Z.pow2_mod di (log_cap i), Z.shiftr di (log_cap i)). |