Open
Description
You can't edit the names of files after creating them.
Workaround: create new file, copy paste content, delete old file.
One issue to consider is that imports might break, e.g. if you've referenced your new file from the main script.
We should see if Pyright has any rename refactoring support we can leverage.