diff options
author | Jason Gross <jagro@google.com> | 2018-08-03 13:45:07 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-08-03 13:45:07 -0400 |
commit | 10335b3bc443a6545a64347db8b8341d08792ed6 (patch) | |
tree | e2432c66736297d3054e92f63e2a26686a270f14 | |
parent | 01704910babc7da4bb0591412cd1640338865751 (diff) |
Add reflect_list_cps_id
-rw-r--r-- | src/Experiments/NewPipeline/LanguageInversion.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index d00efa46c..825881771 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -558,6 +558,10 @@ Module Compilers. apply reflect_list_cps'_id_cons_body; assumption. Qed. + Lemma reflect_list_cps_id {t} {e : expr (base.type.list t)} + : forall T k, @invert_expr.reflect_list_cps _ _ e T k = k (invert_expr.reflect_list e). + Proof. exact (@reflect_list_cps'_id _ e). Qed. + Lemma reflect_list_step {t} {e : expr (base.type.list t)} : invert_expr.reflect_list e = match invert_expr.invert_nil e, invert_expr.invert_cons e with |