From 8fbe7062fad9263094e37a61e1fbe71f20dfd274 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Feb 2022 10:10:34 -0800
Subject: [PATCH] fix: preserve unused let-decls at `Meta.transform`

---
 src/Lean/Meta/Transform.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index 49f6423c27..30a1188c60 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -79,19 +79,19 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
         | Expr.lam n d b c =>
           withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
             visitLambda (fvars.push x) b
-        | e => visitPost (← mkLambdaFVars fvars (← visit (e.instantiateRev fvars)))
+        | e => visitPost (← mkLambdaFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
       let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match e with
         | Expr.forallE n d b c =>
           withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
             visitForall (fvars.push x) b
-        | e => visitPost (← mkForallFVars fvars (← visit (e.instantiateRev fvars)))
+        | e => visitPost (← mkForallFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
       let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match e with
         | Expr.letE n t v b _ =>
           withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x =>
             visitLet (fvars.push x) b
-        | e => visitPost (← mkLetFVars fvars (← visit (e.instantiateRev fvars)))
+        | e => visitPost (← mkLetFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
       let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
         e.withApp fun f args => do
           visitPost (mkAppN (← visit f) (← args.mapM visit))