Commit 2026-09-19 14:57 3258f44a

View on Github →

chore: remove @[expose] from meta definitions (#42318) This PR removes @[expose] from sections where all definitions are meta definitions. (They might not be tagged meta explicitly, but they are meant only for execution and not for proving).

Estimated changes

Modified Mathlib/Lean/ContextInfo.lean

Modified Mathlib/Lean/CoreM.lean

Modified Mathlib/Lean/Elab/InfoTree.lean

Modified Mathlib/Lean/Elab/Tactic/Basic.lean

Modified Mathlib/Lean/Elab/Tactic/Meta.lean

Modified Mathlib/Lean/Exception.lean

Modified Mathlib/Lean/GoalsLocation.lean

Modified Mathlib/Lean/Meta/Basic.lean

Modified Mathlib/Lean/Meta/DiscrTree.lean

Modified Mathlib/Lean/Meta/KAbstractPositions.lean

Modified Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean

Modified Mathlib/Lean/Meta/Simp.lean

Modified Mathlib/Lean/Meta/Tactic/Rewrite.lean

Modified Mathlib/Lean/PrettyPrinter/Delaborator.lean

Modified Mathlib/LinearAlgebra/Matrix/Notation.lean

Modified Mathlib/Order/Notation.lean

Modified Mathlib/Tactic/Module.lean

Modified Mathlib/Tactic/NormNum/Result.lean

modified def Int.rawCast

modified def Nat.rawCast