From 51602bd1ccf7493e53f78afa958238cad14571f2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 18:25:20 +0200 Subject: 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. --- src/ModularArithmetic/Pow2Base.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/ModularArithmetic') 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)). -- cgit v1.2.3