diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-29 13:43:03 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-29 13:43:03 -0400 |
commit | a6fe61b6001857907f40f54e45964d46b754a30d (patch) | |
tree | d26601230012705faabc97ead397f145250707c7 | |
parent | 8eec11bfb6d97a3cbb21e74f26c469157c58e2d8 (diff) |
Fix the sense of op_{get,with}_carry in Saturated
Now it lines up with the things in Z.Definitions
-rw-r--r-- | src/Arithmetic/Saturated.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 5ecb5eebd..14f689322 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -735,10 +735,10 @@ Module Positional. | None => op_get_carry | Some x => op_with_carry x end in dlet carry_result := op' (hd p) (hd q) in - chain_op'_cps (Some (fst carry_result)) (tl p) (tl q) _ + chain_op'_cps (Some (snd carry_result)) (tl p) (tl q) _ (fun carry_pq => f (fst carry_pq, - append (snd carry_result) (snd carry_pq))) + append (fst carry_result) (snd carry_pq))) end. Definition chain_op' {n} c p q := @chain_op'_cps n c p q _ id. Definition chain_op_cps {n} p q {T} f := @chain_op'_cps n None p q T f. |