Commit 2025-07-02 15:47 ff1ed482

View on Github →

chore: deprecate Scott in favour of WithScott (#26619) This type synonym is a duplicate and badly implemented (it is an abbrev). Also fix a few misnamed lemmas about the Scott topology. Closes #26494.

Estimated changes