Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Renaming does not correctly deal with namespaces #2936

Open
mhuisi opened this issue Nov 21, 2023 · 0 comments
Open

Renaming does not correctly deal with namespaces #2936

mhuisi opened this issue Nov 21, 2023 · 0 comments
Labels
bug Something isn't working P-medium We may work on this issue if we find the time server Affects the Lean server code

Comments

@mhuisi
Copy link
Contributor

mhuisi commented Nov 21, 2023

Description

#2462 added support for renaming, but the current implementation does not correctly deal with namespaces:

namespace Bar

  structure Foo where
    a : Nat

  def foobar (f : Foo) : Foo := f

end Bar

def foobar (f : Bar.Foo) : Bar.Foo := f

Renaming Foo here breaks references to Bar.Foo. Similarly, when you rename a type, it does not rename the corresponding namespace, leading to errors because dot notation is suddenly broken for a lot of functions.

Context

Prior discussion in the review comments for #2462.

Steps to Reproduce

  1. Use the MWE above.
  2. Rename Foo.
  3. Observe incorrect renaming behaviour.

Expected behavior: Renaming is aware of namespaces.

Actual behavior: Renaming is not aware of namespaces.

Versions

Commit b97b0ad

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

@mhuisi mhuisi added bug Something isn't working server Affects the Lean server code labels Nov 21, 2023
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Oct 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-medium We may work on this issue if we find the time server Affects the Lean server code
Projects
None yet
Development

No branches or pull requests

2 participants