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

wrong links due to two definitions with same name #219

Open
PhoenixIra opened this issue Sep 28, 2024 · 1 comment
Open

wrong links due to two definitions with same name #219

PhoenixIra opened this issue Sep 28, 2024 · 1 comment

Comments

@PhoenixIra
Copy link

As already issued here: leanprover-community/mathlib4#15415

It seems that the documentation assumes x.abs to be the polymorphic version, but doesn't see that there is also a different version of abs in the local namespace.

This leads to confusion where one may assume that the absolute value of compex numbers is defined non-standard.

Link for reference: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Complex/Arg.html#Complex.arg

@hargoniX
Copy link
Collaborator

This is going to be fixed once we refactor doc string rendering.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants