diff options
Diffstat (limited to 'src/Reflection/Syntax.v')
-rw-r--r-- | src/Reflection/Syntax.v | 6 |
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. |