diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-08 10:45:00 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-08 10:45:00 -0400 |
| commit | bc4db82368c2a75e88e004d1f81cf10bed7bd959 (patch) | |
| tree | ee785d2724c91a6b42826bd48ae80155019d6623 /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | 4028538d1ea1d85f0827ce90fe66a953c033143e (diff) | |
unstuck carry_mul_opt_cps using from_list_default
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index e11186cfb..3d7168c5a 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -486,21 +486,20 @@ Section Multiplication. : mul_opt us vs = mul us vs := proj2_sig (mul_opt_sig us vs). - Definition carry_mul_opt_sig {T:digits->Type} (f:forall d:digits, T d) (us vs : digits) : { x | x = f (carry_mul us vs) }. + Definition carry_mul_opt_sig {T} (f:digits -> T) + (us vs : digits) : { x | x = f (carry_mul us vs) }. Proof. eexists. cbv [carry_mul]. - (* FIXME erewrite <-carry_full_opt_cps_correct by eauto. erewrite <-mul_opt_correct. reflexivity. - *) Defined. - Definition carry_mul_opt_cps {T} (f:forall d:digits, T d) (us vs : digits) : T (carry_mul us vs) + Definition carry_mul_opt_cps {T} (f:digits -> T) (us vs : digits) : T := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig f us vs). - Definition carry_mul_opt_cps_correct {T} (f:forall d:digits, T d) (us vs : digits) + Definition carry_mul_opt_cps_correct {T} (f:digits -> T) (us vs : digits) : carry_mul_opt_cps f us vs = f (carry_mul us vs) := proj2_sig (carry_mul_opt_sig f us vs). End Multiplication. |