From 20de5e544ff04340c1c2f6e471d8549f6fea0986 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 13 May 2017 00:08:54 -0400 Subject: Change definition of add_get_carry The new definition is judgmentally equal to the old one, but is slightly easier to reify. --- src/Util/ZUtil/Definitions.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/ZUtil/Definitions.v') 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. -- cgit v1.2.3