From 8c0bb68ee51a2969b0fdd73fdc18324fcbff88e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 27 Mar 2026 23:10:24 +0100
Subject: [PATCH] perf: prevent unnecessary allocations of EST.Out.ok (#13163)

---
 src/Lean/Meta/Basic.lean             | 8 ++++++++
 src/Lean/Meta/Tactic/Simp/Types.lean | 7 +++++++
 src/Lean/Util/Trace.lean             | 1 +
 3 files changed, 16 insertions(+)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 54c03bbc45..5f6a9cb368 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -717,20 +717,25 @@ def recordSynthPendingFailure (type : Expr) : MetaM Unit := do
       modifyDiag fun { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
         { unfoldCounter, unfoldAxiomCounter, heuristicCounter, instanceCounter, synthPendingFailures := synthPendingFailures.insert type msg }
 
+@[inline]
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
 
+@[inline]
 def getConfig : MetaM Config :=
   return (← read).config
 
+@[inline]
 def getConfigWithKey : MetaM ConfigWithKey :=
   return (← getConfig).toConfigWithKey
 
 /-- Return the array of postponed universe level constraints. -/
+@[inline]
 def getPostponed : MetaM (PersistentArray PostponedEntry) :=
   return (← get).postponed
 
 /-- Set the array of postponed universe level constraints. -/
+@[inline]
 def setPostponed (postponed : PersistentArray PostponedEntry) : MetaM Unit :=
   modify fun s => { s with postponed := postponed }
 
@@ -904,12 +909,15 @@ def mkConstWithFreshMVarLevels (declName : Name) : MetaM Expr := do
   return mkConst declName (← mkFreshLevelMVarsFor info)
 
 /-- Return current transparency setting/mode. -/
+@[inline]
 def getTransparency : MetaM TransparencyMode :=
   return (← getConfig).transparency
 
+@[inline]
 def shouldReduceAll : MetaM Bool :=
   return (← getTransparency) == TransparencyMode.all
 
+@[inline]
 def shouldReduceReducibleOnly : MetaM Bool :=
   return (← getTransparency) == TransparencyMode.reducible
 
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 3751d4c714..6583ec6ae6 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -445,27 +445,33 @@ unsafe def MethodsRef.toMethodsImpl (m : MethodsRef) : Methods :=
 @[implemented_by MethodsRef.toMethodsImpl]
 opaque MethodsRef.toMethods (m : MethodsRef) : Methods
 
+@[inline]
 def getMethods : SimpM Methods :=
   return MethodsRef.toMethods (← read)
 
+@[inline]
 def pre (e : Expr) : SimpM Step := do
   (← getMethods).pre e
 
+@[inline]
 def post (e : Expr) : SimpM Step := do
   (← getMethods).post e
 
 @[inline] def getContext : SimpM Context :=
   readThe Context
 
+@[inline]
 def getConfig : SimpM Config :=
   return (← getContext).config
 
 @[inline] def withParent (parent : Expr) (f : SimpM α) : SimpM α :=
   withTheReader Context (fun ctx => { ctx with parent? := parent }) f
 
+@[inline]
 def getSimpTheorems : SimpM SimpTheoremsArray :=
   return (← readThe Context).simpTheorems
 
+@[inline]
 def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
@@ -473,6 +479,7 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 Returns `true` if `simp` is in `dsimp` mode.
 That is, only transformations that preserve definitional equality should be applied.
 -/
+@[inline]
 def inDSimp : SimpM Bool :=
   return (← readThe Context).inDSimp
 
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 6f1f0a378e..f66c2363a4 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -114,6 +114,7 @@ where
       false
 
 /-- Determine if tracing is available for a given class, checking ancestor classes if appropriate. -/
+@[inline]
 def isTracingEnabledFor (cls : Name) : m Bool := do
   return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptions) cls