From 0c25de529f744cf4b2d848a509cd0d869176fd6d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 28 Jun 2018 16:25:52 -0400 Subject: Start with a better template for carry_square --- src/Experiments/NewPipeline/Toplevel1.v | 3 --- 1 file changed, 3 deletions(-) (limited to 'src/Experiments/NewPipeline/Toplevel1.v') 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) -- cgit v1.2.3