From e8fdfe4193efb27cfbf6d90ff7dcb5e33928aec7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Aug 2022 12:46:46 -0700
Subject: [PATCH] feat: eliminate trivial `let`-declarations

---
 src/Lean/Compiler/Simp.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Compiler/Simp.lean b/src/Lean/Compiler/Simp.lean
index d39b1e0ddc..6a1602bd67 100644
--- a/src/Lean/Compiler/Simp.lean
+++ b/src/Lean/Compiler/Simp.lean
@@ -72,9 +72,13 @@ where
       let mut value := value.instantiateRev xs
       if value.isLambda then
         value ← visitLambda value
-      let type := type.instantiateRev xs
-      let x ← mkLetDecl binderName type value nonDep
-      go body (xs.push x)
+      if value.isFVar then
+        /- Eliminate `let _x_i := _x_j;` -/
+        go body (xs.push value)
+      else
+        let type := type.instantiateRev xs
+        let x ← mkLetDecl binderName type value nonDep
+        go body (xs.push x)
     | _ =>
       let e := e.instantiateRev xs
       if let some casesInfo ← isCasesApp? e then