fix: issues #2669 #2281

src/Lean/Meta/ACLt.lean

@@ -60,8 +60,8 @@ where
       -- Drawback: cost.
       return e
     else match mode with
-      | .reduce => DiscrTree.reduce e (simpleReduce := false)
-      | .reduceSimpleOnly => DiscrTree.reduce e (simpleReduce := true)
+      | .reduce => DiscrTree.reduce e {}
+      | .reduceSimpleOnly => DiscrTree.reduce e { iota := false, proj := .no }
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do

src/Lean/Meta/Basic.lean

@@ -78,14 +78,6 @@ structure Config where
     we may want to notify the caller that the TC problem may be solvable
     later after it assigns `?m`. -/
   isDefEqStuckEx     : Bool := false
-  /--
-    Controls which definitions and theorems can be unfolded by `isDefEq` and `whnf`.
-   -/
-  transparency       : TransparencyMode := TransparencyMode.default
-  /-- If zetaNonDep == false, then non dependent let-decls are not zeta expanded. -/
-  zetaNonDep         : Bool := true
-  /-- When `trackZeta == true`, we store zetaFVarIds all free variables that have been zeta-expanded. -/
-  trackZeta          : Bool := false
   /-- Enable/disable the unification hints feature. -/
   unificationHints   : Bool := true
   /-- Enables proof irrelevance at `isDefEq` -/
@@ -99,8 +91,24 @@ structure Config where
   assignSyntheticOpaque : Bool := false
   /-- Enable/Disable support for offset constraints such as `?x + 1 =?= e` -/
   offsetCnstrs          : Bool := true
+  /--
+    Controls which definitions and theorems can be unfolded by `isDefEq` and `whnf`.
+   -/
+  transparency       : TransparencyMode := TransparencyMode.default
+  /--
+  When `trackZeta = true`, we track all free variables that have been zeta-expanded.
+  That is, suppose the local context contains
+  the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaFVarIds`.
+  We use `trackZeta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
+  When we find these declarations we set their `nonDep` flag with `true`.
+  To find these let-declarations in a given term `s`, we
+  1- Reset `State.zetaFVarIds`
+  2- Set `trackZeta := true`
+  3- Type-check `s`.
+  -/
+  trackZeta          : Bool := false
   /-- Eta for structures configuration mode. -/
-  etaStruct             : EtaStructMode := .all
+  etaStruct          : EtaStructMode := .all
 
 /--
   Function parameter information cache.
@@ -366,7 +374,7 @@ section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
-  modify fun ⟨mctx, cache, zetaFVarIds, postponed⟩ => ⟨mctx, f cache, zetaFVarIds, postponed⟩
+  modify fun { mctx, cache, zetaFVarIds, postponed } => { mctx, cache := f cache, zetaFVarIds, postponed }
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
@@ -781,6 +789,9 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withConfig (f : Config → Config) : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
 
+/--
+Executes `x` tracking zeta reductions `Config.trackZeta := true`
+-/
 @[inline] def withTrackingZeta (x : n α) : n α :=
   withConfig (fun cfg => { cfg with trackZeta := true }) x