Add invert_LetIn

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 021e9a21d..39ca3059b 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -378,6 +378,11 @@ Section language.
            | Pair _ x _ y => Some (x, y)%core
            | _ => None
            end.
+      Definition invert_LetIn {var A} (e : @exprf var A) : option { B : _ & exprf B * (interp_flat_type_gen var B -> exprf A) }%type
+        := match e in @exprf _ t return option { B : _ & _ * (_ -> exprf t) }%type with
+           | LetIn _ ex _ eC => Some (existT _ _ (ex, eC))
+           | _ => None
+           end.
     End misc.
 
     Section wf.
@@ -485,6 +490,7 @@ Global Arguments interp {_ _ _} interp_op {t} _.
 Global Arguments interpf {_ _ _} interp_op {t} _.
 Global Arguments invert_Const {_ _ _ _ _} _.
 Global Arguments invert_Pair {_ _ _ _ _ _} _.
+Global Arguments invert_LetIn {_ _ _ _ _} _.
 
 Module Export Notations.
   Notation "A * B" := (@Prod _ A B) : ctype_scope.