test: see if we can remove let_fun to move withSetOptionIn

src/Lean/Elab/Binders.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.Elab.Match
 meta import Lean.Parser.Tactic
-import Lean.Linter.Basic
 
 public section
 
@@ -943,12 +942,6 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : L
 @[builtin_term_elab «have»] def elabHaveDecl : TermElab :=
   fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }
 
-@[builtin_term_elab «let_fun»] def elabLetFunDecl : TermElab :=
-  fun stx expectedType? => do
-    withRef stx <| Linter.logLintIf Linter.linter.deprecated stx[0]
-      "`let_fun` has been deprecated in favor of `have`"
-    elabLetDeclCore stx expectedType? { nondep := true }
-
 @[builtin_term_elab «let_delayed»] def elabLetDelayedDecl : TermElab :=
   fun stx expectedType? => elabLetDeclCore stx expectedType? { postponeValue := true }
 

src/Lean/Elab/Command.lean

@@ -859,19 +859,6 @@ def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : Cor
   -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
   MonadExcept.ofExcept (← liftCommandElabMCore (observing cmd) throwOnError)
 
-/--
-Given a command elaborator `cmd`, returns a new command elaborator that
-first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
--/
-partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
-  if stx.getKind == ``Lean.Parser.Command.in &&
-     stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
-      Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[2]
-  else
-    cmd stx
-
 export Elab.Command (Linter addLinter)
 
 end Lean

src/Lean/Elab/SetOption.lean

@@ -42,14 +42,22 @@ where
         {indentExpr defValType}"
     | _ => throwUnconfigurable optionName
 
-def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
+/--
+Elaborates `id` as an identifier representing an option name with value given by `val`.
+
+Validates that `val` has the correct type for values of the option `id`, and returns the updated
+`Options`. Does **not** update the options in the monad `m`.
+
+If `addInfo := true` (the default), adds completion info and elaboration info to the infotrees.
+-/
+def elabSetOption (id : Syntax) (val : Syntax) (addInfo := true) : m Options := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
-  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
+  if addInfo then addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
-  pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
+  if addInfo then pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
   let rec setOption (val : DataValue) : m Options := do
     validateOptionValue optionName decl val
     return (← getOptions).insert optionName val

src/Lean/Expr.lean

@@ -1998,50 +1998,6 @@ def setAppPPExplicitForExposingMVars (e : Expr) : Expr :=
     mkAppN f args |>.setPPExplicit true
   | _      => e
 
-/--
-Returns true if `e` is an expression of the form `letFun v f`.
-Ideally `f` is a lambda, but we do not require that here.
-Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `false`.
--/
-@[deprecated Expr.isHave (since := "2025-06-29")]
-def isLetFun (e : Expr) : Bool := e.isAppOfArity ``letFun 4
-
-/--
-Recognizes a `let_fun` expression.
-For `let_fun n : t := v; b`, returns `some (n, t, v, b)`, which are the first four arguments to `Lean.Expr.letE`.
-Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `none`.
-
-`let_fun` expressions are encoded as `letFun v (fun (n : t) => b)`.
-They can be created using `Lean.Meta.mkLetFun`.
-
-If in the encoding of `let_fun` the last argument to `letFun` is eta reduced, this returns `Name.anonymous` for the binder name.
--/
-@[deprecated Expr.isHave (since := "2025-06-29")]
-def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
-  match e with
-  | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f =>
-    match f with
-    | .lam n _ b _ => some (n, t, v, b)
-    | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
-  | _ => none
-
-/--
-Like `Lean.Expr.letFun?`, but handles the case when the `let_fun` expression is possibly applied to additional arguments.
-Returns those arguments in addition to the values returned by `letFun?`.
--/
-@[deprecated Expr.isHave (since := "2025-06-29")]
-def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Expr) := do
-  guard <| 4 ≤ e.getAppNumArgs
-  guard <| e.isAppOf ``letFun
-  let args := e.getAppArgs
-  let t := args[0]!
-  let v := args[2]!
-  let f := args[3]!
-  let rest := args.extract 4 args.size
-  match f with
-  | .lam n _ b _ => some (rest, n, t, v, b)
-  | _ => some (rest, .anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
-
 /-- Maps `f` on each immediate child of the given expression. -/
 @[specialize]
 def traverseChildren [Applicative M] (f : Expr → M Expr) : Expr → M Expr

src/Lean/Linter/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.MonadEnv
+public import Lean.Elab.Command
 
 public section
 
@@ -89,3 +90,23 @@ Whether a linter option is enabled or not is determined by the following sequenc
 def logLintIf [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
   if getLinterValue linterOption (← getLinterOptions) then logLint linterOption stx msg
+
+/--
+Given a command elaborator `cmd`, returns a new command elaborator that
+first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
+
+This is expected to be used in linters, after elaboration is complete. It is not appropriate for
+ordinary elaboration of `set_option`s, since it
+* does not update the infotrees with elaboration info from elaborating the `set_option` commands
+* silently ignores failures in setting the given options (e.g. we do not error if the option is
+  unknown or the wrong type of value is provided)
+-/
+partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
+  if stx.getKind == ``Lean.Parser.Command.in &&
+     stx[0].getKind == ``Lean.Parser.Command.set_option then
+      -- Do not modify the infotrees when elaborating, and silently ignore errors.
+      let opts ← try Elab.elabSetOption stx[0][1] stx[0][3] (addInfo := false) catch _ => getOptions
+      Command.withScope (fun scope => { scope with opts }) do
+        withSetOptionIn cmd stx[2]
+  else
+    cmd stx

src/Lean/Linter/List.lean

@@ -179,7 +179,6 @@ def indexLinter : Linter
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
-      if let .context _ _ := t then -- Only consider info trees with top-level context
       for (idxStx, n) in numericalIndices t do
         if let .str _ n := n then
           if !allowedIndices.contains (stripBinderName n) then
@@ -236,32 +235,31 @@ def listVariablesLinter : Linter
     if (← get).messages.hasErrors then return
     if ! (← getInfoState).enabled then return
     for t in ← getInfoTrees do
-      if let .context _ _ := t then -- Only consider info trees with top-level context
-        let binders ← binders t
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedListNames.contains n then
-            -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
-            unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `List` name: {n}"
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedArrayNames.contains n then
-            -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
-            unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `Array` name: {n}"
-        for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
-          if let .str _ n := n then
-          let n := stripBinderName n
-          if !allowedVectorNames.contains n then
-            -- Allow `xss` for `Vector (Vector α)`
-            unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
-              Linter.logLint linter.listVariables stx
-                m!"Forbidden variable appearing as a `Vector` name: {n}"
+      let binders ← binders t
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedListNames.contains n then
+          -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
+          unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `List` name: {n}"
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedArrayNames.contains n then
+          -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
+          unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `Array` name: {n}"
+      for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
+        if let .str _ n := n then
+        let n := stripBinderName n
+        if !allowedVectorNames.contains n then
+          -- Allow `xss` for `Vector (Vector α)`
+          unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
+            Linter.logLint linter.listVariables stx
+              m!"Forbidden variable appearing as a `Vector` name: {n}"
 
 builtin_initialize addLinter listVariablesLinter
 

src/Lean/Meta/AppBuilder.lean

@@ -37,25 +37,6 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
   return mkExpectedTypeHintCore e expectedType u
 
-/--
-`mkLetFun x v e` creates `letFun v (fun x => e)`.
-The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
--/
-@[deprecated mkLetFVars (since := "2026-06-29")]
-def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
-  -- If `x` is an `ldecl`, then the result of `mkLambdaFVars` is a let expression.
-  let ensureLambda : Expr → Expr
-    | .letE n t _ b _ => .lam n t b .default
-    | e@(.lam ..)     => e
-    | _               => unreachable!
-  let f ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] e
-  let ety ← inferType e
-  let α ← inferType x
-  let β ← ensureLambda <$> mkLambdaFVars (usedLetOnly := false) #[x] ety
-  let u1 ← getLevel α
-  let u2 ← getLevel ety
-  return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
-
 /-- Returns `a = b`. -/
 def mkEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a

src/Lean/Meta/ExprDefEq.lean

@@ -1689,9 +1689,9 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
 
     theorem p_of_q : q x → p x := sorry
 
-    theorem pletfun : p (let_fun x := 0; x + 1) := by
-      -- ⊢ p (let_fun x := 0; x + 1)
-      apply p_of_q -- If we eagerly consume all metadata, the let_fun annotation is lost during `isDefEq`
+    theorem phave : p (have x := 0; x + 1) := by
+      -- ⊢ p (have x := 0; x + 1)
+      apply p_of_q -- If we eagerly consume all metadata, the `have` annotation is lost during `isDefEq`
       -- ⊢ q ((fun x => x + 1) 0)
       sorry
     ```

src/Lean/Parser/Term.lean

@@ -519,11 +519,6 @@ creating a *nondependent* let expression.
 @[builtin_term_parser] def «have» := leading_parser:leadPrec
   withPosition ("have" >> letConfig >> letDecl) >> optSemicolon termParser
 /--
-`let_fun x := v; b` is deprecated syntax sugar for `have x := v; b`.
--/
-@[builtin_term_parser] def «let_fun»     := leading_parser:leadPrec
-  withPosition ((symbol "let_fun " <|> "let_λ ") >> letDecl) >> optSemicolon termParser
-/--
 `let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
 -/
 @[builtin_term_parser] def «let_delayed» := leading_parser:leadPrec

tests/lean/consumePPHint.lean

@@ -7,7 +7,7 @@ opaque q : Nat → Prop
 
 theorem p_of_q : q x → p x := sorry
 
-theorem pletfun : p (have x := 0; x + 1) := by
+theorem phave : p (have x := 0; x + 1) := by
   -- ⊢ p (have x := 0; x + 1)
   apply p_of_q
   trace_state -- `have` should not be consumed.

tests/lean/run/index_variables_linter.lean

@@ -50,3 +50,21 @@ Note: This linter can be disabled with `set_option linter.indexVariables false`
 -/
 #guard_msgs in
 example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl
+
+/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
+context-free info nodes (#11313) -/
+
+set_option linter.indexVariables false
+
+/--
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
+---
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
+-/
+#guard_msgs in
+set_option linter.indexVariables true in
+example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl

tests/lean/run/list_variables_linter.lean

@@ -50,3 +50,21 @@ Note: This linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l : Array Nat) : l = l := rfl
+
+/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
+context-free info nodes (#11313) -/
+
+set_option linter.listVariables false
+
+/--
+warning: Forbidden variable appearing as a `Array` name: l
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
+---
+warning: Forbidden variable appearing as a `Array` name: l
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
+-/
+#guard_msgs in
+set_option linter.listVariables true in
+example (l : Array Nat) : l = l := rfl