diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 00:08:54 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-13 18:42:29 -0400 |
| commit | 20de5e544ff04340c1c2f6e471d8549f6fea0986 (patch) | |
| tree | 52858d6bb45ae93646577326dd1925cd177c7a30 /src/Util/ZUtil/Definitions.v | |
| parent | cf76a8c3fd1d240545bd87150aab1081d3f7c9a8 (diff) | |
Change definition of add_get_carry
The new definition is judgmentally equal to the old one, but is slightly
easier to reify.
Diffstat (limited to 'src/Util/ZUtil/Definitions.v')
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index a8dbc5e96..a74e4b8f4 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -15,5 +15,5 @@ Module Z. Definition add_with_get_carry (bitwidth : Z) (c : Z) (x y : Z) : Z * Z := get_carry bitwidth (add_with_carry c x y). Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z - := get_carry bitwidth (x + y). + := add_with_get_carry bitwidth 0 x y. End Z. |