Zulip Chat Archive
Stream: mathlib4
Topic: PartialHomeomorph.restr naming
Luigi Massacci (Sep 25 2024 at 19:26):
Is there a reason docs#PartialHomeomorph.restr is called like that, as opposed to .restrict like everything (?) else? Any downsides to renaming it for better library consistency?
Johan Commelin (Sep 26 2024 at 07:15):
Afaict, please go ahead and rename it
Ruben Van de Velde (Sep 26 2024 at 07:33):
And add deprecated aliases
Last updated: May 02 2025 at 03:31 UTC