-
Notifications
You must be signed in to change notification settings - Fork 259
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
[Merged by Bors] - Add missing readmes #6031
Conversation
Try to adhere to the guidelines for mathlib. They will be much less strictly enforced for the archive, but we still want you to adhere to all the conventions that make maintenance easier. This ensures that when mathlib is changing, the mathlib maintainers can fix these contributions without much effort. Here are the guidelines: | ||
- The [style guide](https://leanprover-community.github.io/contribute/style.html) for contributors. | ||
- The [git commit conventions](https://github.com/leanprover-community/lean4/blob/master/doc/commit_convention.md). | ||
- You don't have to follow the [naming conventions](https://leanprover-community.github.io/contribute/naming.html). |
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.
Still about Lean 3.
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.
This link is supposed to lead to the Lean4 one though, right? Which is to say, the problem is at the page it links to.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
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.
Thanks 🎉
bors merge
These are copied with minimal modification from mathlib3.
Build failed (retrying...): |
These are copied with minimal modification from mathlib3.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
These are copied with minimal modification from mathlib3.
These are copied with minimal modification from mathlib3.
These are copied with minimal modification from mathlib3.