Commit 2026-08-25 23:31 5f181380

View on Github →

chore: remove some backward.privateInPublic by adjusting visibility (#42557) This PR removes a batch of set_option backward.privateInPublic true by adjusting visibility according to the following rules:

If a theorem is about an already-private definition, it too may as well be private.
We can @[no_expose] defs that use private definitions
We can private definitions that have no consumers besides an exposed body

Estimated changes

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Fintype/EquivFin.lean

Modified Mathlib/Data/Nat/Find.lean

Modified Mathlib/Data/Seq/Parallel.lean

modified def Computation.parallel

deleted theorem Computation.terminates_parallel.aux

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Encodable/Basic.lean

modified def Encodable.choose

deleted def Encodable.chooseX

Modified Mathlib/Logic/Equiv/Multiset.lean

modified def encodeMultiset

Modified Mathlib/Logic/Godel/GodelBetaFunction.lean

deleted theorem Nat.coprimes_lt

modified def Nat.unbeta

Modified Mathlib/Order/DirectedInverseSystem.lean

Modified Mathlib/Order/Lattice/Congruence.lean

modified def LatticeCon.mk'