From 082e0c4d466bf37a0fc5243a4255a92747342e68 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 4 Dec 2024 09:39:58 +0100
Subject: [PATCH] do not pull let out of lambdas by default in lsimp

---
 SciLean/Tactic/LSimp/Main.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/SciLean/Tactic/LSimp/Main.lean b/SciLean/Tactic/LSimp/Main.lean
index 7fbb0b2b..e8e52a68 100644
--- a/SciLean/Tactic/LSimp/Main.lean
+++ b/SciLean/Tactic/LSimp/Main.lean
@@ -362,13 +362,17 @@ partial def simpLambda (e : Expr) : LSimpM Result := do
   withParent e <| lambdaTelescopeDSimp e fun xs e => do
     withoutModifyingLCtx pure do withoutModifyingCache do withNewLemmas xs do
       let r ← lsimp e
+
       let (eNew,vars)  ← xs.foldrM (init:=(r.expr,r.vars)) fun x (e,vars) => do
         let deps ← collectForwardDeps #[x] false
         let (vars', vars) := vars.partition deps.contains
         let e ← mkLambdaFVars (#[x] ++ vars') e
         pure (e,vars)
       let eNew ← mkLambdaFVars vars eNew
+
       let r ← r.bindVars
+      let pullLetOutOfLambda := false -- todo: turn this into `lsimp` config option
+      let eNew ← if pullLetOutOfLambda then pure eNew else mkLambdaFVars xs r.expr
       match r.proof? with
       | none   => return { expr := eNew }
       | some h =>