Commit 2026-06-16 13:17 d18bb636

chore: make _root_.toContinuousMap reducible (#40477) If a structure extends ContinuousMap and also carries an instance of ContinuousMapClass then it will have two toContinuousMap functions available to it. Without this change, at non-reducible transparency Lean is unable to see that these two are defeq (assuming we have written a sane API and they are!). The motivating example is the Path structure where the lack of this reducibility was responsible for some backward.isDefEq.respectTransparency false in #33108.