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.