diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-22 17:01:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-22 17:01:31 -0400 |
| commit | 055d75c242af8cbf49f767ca0e3636ae3c257ae0 (patch) | |
| tree | 28ba27f866e3ed999e5e34cefe5c5e74fc3fabbd /src/Reflection/CountLets.v | |
| parent | 9c161a63a918b266df3975110ed0244dc69eaf79 (diff) | |
Also count lets in operations and pairs
Diffstat (limited to 'src/Reflection/CountLets.v')
| -rw-r--r-- | src/Reflection/CountLets.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v index 643bb1bf5..64c46d58a 100644 --- a/src/Reflection/CountLets.v +++ b/src/Reflection/CountLets.v @@ -33,6 +33,8 @@ Section language. := match e with | LetIn tx _ _ eC => count_type_let tx + @count_lets_genf _ (eC (SmartValf var mkVar tx)) + | Op _ _ _ e => @count_lets_genf _ e + | Pair _ ex _ ey => @count_lets_genf _ ex + @count_lets_genf _ ey | _ => 0 end. Definition count_lets_gen {t} (e : expr t) : nat |