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 | |
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.
-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)). |