[Merged by Bors] - chore(Tactic): move StacksAttribute to CrossRefAttribute#39257
[Merged by Bors] - chore(Tactic): move StacksAttribute to CrossRefAttribute#39257jcommelin wants to merge 2 commits into
Conversation
This PR moves StacksAttribute.lean to CrossRefAttribute.lean both in Mathlib/Tactic/ and in MathlibTest/. In the future, we can refactor the file to abstract over the type of cross-references. Currently, cross-reference attributes are implemented for the Stacks Project and Kerodon. A good candidate for a future PR is to add an attribute for Wikidata identifiers.
PR summary 53f8a93a77Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
bors d+ |
|
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for getting this started! |
|
As this PR is labelled bors merge |
This PR moves StacksAttribute.lean to CrossRefAttribute.lean both in Mathlib/Tactic/ and in MathlibTest/. In the future, we can refactor the file to abstract over the type of cross-references. Currently, cross-reference attributes are implemented for the Stacks Project and Kerodon. A good candidate for a future PR is to add an attribute for Wikidata identifiers.
|
Pull request successfully merged into master. Build succeeded: |
This PR moves StacksAttribute.lean to CrossRefAttribute.lean
both in Mathlib/Tactic/ and in MathlibTest/.
In the future, we can refactor the file to abstract over the type of
cross-references. Currently, cross-reference attributes are implemented
for the Stacks Project and Kerodon.
A good candidate for a future PR is to add an attribute for Wikidata
identifiers.