-
Notifications
You must be signed in to change notification settings - Fork 88
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
feat: add alias tactic #184
Conversation
3674d65
to
de40d83
Compare
Std/Tactic/Alias.lean
Outdated
|
||
TODO: Move this declaration to a more central location. | ||
-/ | ||
def appendNamespace (ns : Name) : Name → Name |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe this should be moved to a central location in Std? Other than that, LGTM
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
or in lean... I know this is reimplemented at least 3 times in lean core
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm happy to change this given a pointer to an implementation in core.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I couldn't find this exact thing in core but I did simplify the definition a bit.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is now a PR in core: lean4#2341.
I added support for protected aliases and I added a Mathlib patch. |
Obsoleted by #200 |
Move from Mathlib. Added support for protected aliases.