From fe0c2f54075c9f5c6805ee165dbf9df8b8058693 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 12:56:36 -0400 Subject: Add InterpEta It's a version of [Interp] that works even when there are destructuring lets. --- src/Reflection/Eta.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Reflection/Eta.v') diff --git a/src/Reflection/Eta.v b/src/Reflection/Eta.v index eda74f4a5..d40267858 100644 --- a/src/Reflection/Eta.v +++ b/src/Reflection/Eta.v @@ -63,3 +63,13 @@ Section language. Definition ExprEta' {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t)) := fun var => expr_eta' (e var). End language. +(* put these outside the section so the argument order lines up with + [interp] and [Interp] *) +Definition interp_eta {base_type_code interp_base_type op} interp_op + {t} (e : @expr base_type_code op interp_base_type t) + : interp_type interp_base_type t + := interp_flat_type_eta (interp interp_op e). +Definition InterpEta {base_type_code interp_base_type op} interp_op + {t} (e : @Expr base_type_code op t) + : interp_type interp_base_type t + := interp_eta interp_op (e _). -- cgit v1.2.3