diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-19 16:41:20 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-19 16:41:20 -0700 |
| commit | 24c557e38fac865e059832a17d6ae1591284bc42 (patch) | |
| tree | 74445acbdf89fb361fe49710eea97c76afbc14c0 /src | |
| parent | 64d7f47edd9148c3d4d78489d3bfaf1dd35423dc (diff) | |
Add a distr_length database
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ListUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8b92ef4fa..1032e1dc2 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -38,6 +38,8 @@ Hint Rewrite @prod_length : distr_length. +Hint Extern 1 => progress autorewrite with distr_length in * : distr_length. + Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l). Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := |