diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-16 16:04:04 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-02-18 19:25:23 -0500 |
| commit | 80ca8cf8825f87c2f5c8da0fc1cd63168f30054d (patch) | |
| tree | 8614c7be708fbfe6aaa164f5aad2c47e04194a17 /src | |
| parent | aea2a134c95c55f7f5a6501efc48a3624cad6ca4 (diff) | |
Rename carry_mulmod_correct to eval_carry_mulmod to fit with other lemmas
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 8b216ef57..98d7badf1 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -299,7 +299,7 @@ Module Positional. Section Positional. (Hw_div_nz : forall i : nat, weight (S i) / weight i <> 0), (eval n carry_mulmod) mod (s - Associational.eval c) = (eval n f * eval n g) mod (s - Associational.eval c)) - As carry_mulmod_correct. + As eval_carry_mulmod. Proof. intros. erewrite <-eval_mulmod with (s:=s) (c:=c) @@ -4275,7 +4275,7 @@ Section rcarry_mul. (** This code may eventually be useful; it proves that [check_args] is sufficient to satisfy the preconditions of - [carry_mulmod_correct] *) + [eval_carry_mulmod] *) (* << break_innermost_match_hyps; try solve [ exfalso; clear -Hrv; discriminate ]; []. |