diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Rewriter.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 5fe127ca0..599a7d34e 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -1174,6 +1174,16 @@ In the RHS, the follow notation applies: (??{list ??} ++ ??{list ??}) (fun _ xs _ ys => rlist_rect_cast ys (fun x _ xs_ys => x :: xs_ys) xs) ; make_rewrite + (#pident.List_firstn @ #?ℕ @ ??{list ??}) + (fun n _ xs + => xs <- reflect_list_cps xs; + reify_list (List.firstn n xs)) + ; make_rewrite + (#pident.List_skipn @ #?ℕ @ ??{list ??}) + (fun n _ xs + => xs <- reflect_list_cps xs; + reify_list (List.skipn n xs)) + ; make_rewrite (#pident.List_rev @ ??{list ??}) (fun _ xs => xs <- reflect_list_cps xs; |