diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-18 00:13:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-18 11:02:20 -0400 |
| commit | 1636b6872b4947a238b433ad904899548ff8edfd (patch) | |
| tree | 89f87b4512e9f2d589ef36a756b9ceda63f2125b /src/Arithmetic/Core.v | |
| parent | cb95f631364d06620ce24ff01cf44b7d2035a705 (diff) | |
Add some more things to basesystem_partial_evaluation_unfolder
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index f3c435a09..2c6ac52db 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1018,6 +1018,14 @@ Hint Unfold Z.add_get_carry_full : basesystem_partial_evaluation_unfolder. +Hint Unfold + B.limb ListUtil.sum ListUtil.sum_firstn + CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 + Decidable.dec Decidable.dec_eq_Z + id_tuple_with_alt id_tuple'_with_alt + Z.add_get_carry_full Z.mul_split + : basesystem_partial_evaluation_unfolder. + Ltac basesystem_partial_evaluation_unfolder t := eval cbv |