From 668ea5d4857ef81fc6bb8e83161c4590398c7ca0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 17 Nov 2017 19:26:08 -0500
Subject: Add interpf_SmartVarf

---
 src/Compilers/SmartMap.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/Compilers')

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)
-- 
cgit v1.2.3