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

[Merged by Bors] - feat: Port Data.Rat.Sqrt #1252

Closed

Conversation

aricursion
Copy link
Collaborator

@aricursion aricursion commented Dec 28, 2022

Hi! This is my first port so I picked something pretty small. This is the initial commit where everything compiles properly, but I haven't looked at style guidelines super thoroughly yet. Please give any feedback that you have!

Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good as far as I can tell without CI. Please ask for push access to the main repository on zulip, so you can make branches there going forward.

@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. labels Dec 29, 2022
@aricursion
Copy link
Collaborator Author

will do!

@ChrisHughes24
Copy link
Member

bors merge

bors bot pushed a commit that referenced this pull request Dec 29, 2022
Hi! This is my first port so I picked something pretty small. This is the initial commit where everything compiles properly, but I haven't looked at style guidelines super thoroughly yet. Please give any feedback that you have!

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
@bors
Copy link

bors bot commented Dec 29, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Port Data.Rat.Sqrt [Merged by Bors] - feat: Port Data.Rat.Sqrt Dec 29, 2022
@bors bors bot closed this Dec 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants