diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-28 16:25:52 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-07-03 19:28:55 -0400 |
| commit | 0c25de529f744cf4b2d848a509cd0d869176fd6d (patch) | |
| tree | 091660379b673de7c5a20dda44007351d1624fb1 /src/Experiments/NewPipeline/Toplevel1.v | |
| parent | 243fab24ba4f48d742ac6cb5998a0df0ef8c188d (diff) | |
Start with a better template for carry_square
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index a0ecc885b..68c8555dd 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -664,9 +664,6 @@ Derive carry_mul_gen Proof. Time cache_reify (). Time Qed. Hint Extern 1 (_ = carry_mulmod _ _ _ _ _ _ _ _) => simple apply carry_mul_gen_correct : reify_gen_cache. -Definition carry_squaremod limbwidth_num limbwidth_den s c n idxs f : list Z - := carry_mulmod limbwidth_num limbwidth_den s c n idxs f f. - Derive carry_square_gen SuchThat (forall (limbwidth_num limbwidth_den : Z) (f : list Z) |