Commit 2025-11-09 19:24 bd350e6b

View on Github →

chore: adaptations for batteries#1496 (#31437)

Estimated changes

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Expr.addLocalVarInfoForBinderIdent

Modified Mathlib/Tactic/Cases.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Core.lean

Modified Mathlib/Tactic/GeneralizeProofs.lean

deleted structure Mathlib.Tactic.GeneralizeProofs.AContext

deleted structure Mathlib.Tactic.GeneralizeProofs.AState

deleted structure Mathlib.Tactic.GeneralizeProofs.Config

deleted structure Mathlib.Tactic.GeneralizeProofs.GState

deleted def Mathlib.Tactic.GeneralizeProofs.MAbs.findProof?

deleted def Mathlib.Tactic.GeneralizeProofs.MAbs.insertProof

deleted def Mathlib.Tactic.GeneralizeProofs.MAbs.withLocal

deleted def Mathlib.Tactic.GeneralizeProofs.MAbs.withRecurse

deleted def Mathlib.Tactic.GeneralizeProofs.MGen.insertFVar

deleted def Mathlib.Tactic.GeneralizeProofs.MGen.runMAbs

deleted def Mathlib.Tactic.GeneralizeProofs.appArgExpectedTypes

deleted def Mathlib.Tactic.GeneralizeProofs.initialPropToFVar

deleted def Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly

Deleted MathlibTest/GeneralizeProofs.lean

deleted theorem zulip1.good

deleted def zulip1.p

deleted theorem zulip1.t

deleted theorem zulip1.was_bad

Modified lake-manifest.json

Modified scripts/noshake.json