diff options
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/SmartMap.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Compilers/SmartMap.v b/src/Compilers/SmartMap.v index a7ba64712..b02bba2a1 100644 --- a/src/Compilers/SmartMap.v +++ b/src/Compilers/SmartMap.v @@ -424,6 +424,16 @@ Section interp_lemmas. Local Notation exprfb := (fun t => exprf _ op (Tbase t)). + Lemma interpf_SmartVarf + {t} (e : interp_flat_type _ t) + : @interpf _ interp_base_type _ interp_op _ (SmartVarf (var:=interp_base_type) e) + = e. + Proof. + induction t as [ t | | A IHA B IHB ]; try destruct e; try reflexivity. + rewrite !SmartVarf_Pair; cbn; rewrite IHA, IHB. + reflexivity. + Qed. + Lemma interpf_SmartPairf' {t} (e : interp_flat_type exprfb t) : @interpf _ interp_base_type _ interp_op _ (SmartPairf e) |