diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-26 13:23:40 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-06-26 13:23:40 -0400 |
| commit | 6d3702edad1a69a08565a288f1153b4853ba3b25 (patch) | |
| tree | 2bd599356721995432c4edf5f803f425024cf668 /src/Util/ZUtil/AddGetCarry.v | |
| parent | baa585b4fce11c7ce4eb4493c98137fd87e74c0c (diff) | |
Slightly better definitions of some ZUtil functions
This way we can just directly reify most of the primitives we care
about.
Diffstat (limited to 'src/Util/ZUtil/AddGetCarry.v')
| -rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index e8f8d883d..5b8cbf13e 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -1,5 +1,4 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.Prod. @@ -64,7 +63,7 @@ Module Z. Z.add_get_carry_full Z.add_with_get_carry_full Z.add_get_carry Z.add_with_get_carry Z.add_with_carry Z.sub_get_borrow_full Z.sub_with_get_borrow_full - Z.sub_get_borrow Z.sub_with_get_borrow Z.sub_with_borrow. + Z.sub_get_borrow Z.sub_with_get_borrow Z.sub_with_borrow Let_In. Lemma add_get_carry_full_mod s x y : fst (Z.add_get_carry_full s x y) = (x + y) mod s. |