diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-17 19:26:08 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-17 19:26:08 -0500 |
| commit | 668ea5d4857ef81fc6bb8e83161c4590398c7ca0 (patch) | |
| tree | 6e124dfbdea400d1968f03d628f8207ffd6126e0 /src/Compilers | |
| parent | a96f7f9c31713cee36949e7a7e8c52227f301014 (diff) | |
Add interpf_SmartVarf
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) |