From 10335b3bc443a6545a64347db8b8341d08792ed6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 Aug 2018 13:45:07 -0400 Subject: Add reflect_list_cps_id --- src/Experiments/NewPipeline/LanguageInversion.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src') 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 -- cgit v1.2.3