diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 19:44:36 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-14 19:48:44 -0400 |
| commit | cb50e3f370588e02d1726363d5b64bd00ef49f5b (patch) | |
| tree | a92b54fa9f2569af6b4382f037f3220bffebe813 /src/Specific/IntegrationTestSquare.v | |
| parent | 1c8c702b7ee5b1f62496e6fdf9070332a344f4f7 (diff) | |
Use specialized square in ladderstep
Diffstat (limited to 'src/Specific/IntegrationTestSquare.v')
| -rw-r--r-- | src/Specific/IntegrationTestSquare.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v index b0b5e5b5a..eb91a13ff 100644 --- a/src/Specific/IntegrationTestSquare.v +++ b/src/Specific/IntegrationTestSquare.v @@ -54,8 +54,8 @@ Section BoundedField25p5. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig square_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a a)). - change (proj1_sig carry_sig (proj1_sig square_sig ?a ?a)) with (carry_squareZ a). + set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a)). + change (proj1_sig carry_sig (proj1_sig square_sig ?a)) with (carry_squareZ a). context_to_dlet_in_rhs carry_squareZ. cbv beta iota delta [carry_squareZ proj1_sig square_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. reflexivity. |