Leonardo de Moura dadc91de4b feat: backward.isDefEq.respectTransparency (part 1) (#12338) ... This PR implements preparatory work for #12179. It implements a new feature in `isDefEq` to ensure it does not increase the transparency level to `.default` when checking definitionally equality of implicit arguments. This transparency level bump was introduced in Lean 3, but it is not a performance issue and is affecting Mathlib. This PR adds the new feature, but it is disabled by default.		2026-02-06 06:09:17 +00:00
..
src	feat: backward.isDefEq.respectTransparency (part 1) (#12338)	2026-02-06 06:09:17 +00:00
stdlib	chore: update stage0	2026-02-05 13:41:34 +11:00