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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - port: Nat.sqrt extension for norm_num #4027

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - port: Nat.sqrt extension for norm_num #4027

wants to merge 6 commits into from

Conversation

kmill
Copy link
Contributor

@kmill kmill commented May 16, 2023

Open in Gitpod

@kmill kmill added the t-meta Tactics, attributes or user commands label May 16, 2023
@kmill kmill added the awaiting-review The author would like community review of the PR label May 16, 2023
@kmill
Copy link
Contributor Author

kmill commented May 16, 2023

@digama0 Here's a port of your Nat.sqrt extension. Should I be including any porting header for this meta file since it came from the theory folder?

digama0
digama0 reviewed May 16, 2023
View reviewed changes
test/norm_num_ext.lean Outdated Show resolved Hide resolved
@semorrison
Copy link
Contributor

I think no need for a porting header.

@kmill @digama0
Update test/norm_num_ext.lean
34f9a89 
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 23, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 25, 2023
@digama0
Copy link
Member

digama0 commented May 27, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 27, 2023
bors bot pushed a commit that referenced this pull request May 27, 2023
@kmill
port: Nat.sqrt extension for norm_num (#4027)
23055ec
@bors
Copy link

bors bot commented May 27, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title port: Nat.sqrt extension for norm_num [Merged by Bors] - port: Nat.sqrt extension for norm_num May 27, 2023
@bors bors bot closed this May 27, 2023
@bors bors bot deleted the kmill_normnum_nat_sqrt branch May 27, 2023 12:33
Parcly-Taxel added a commit that referenced this pull request Jun 5, 2023
@Parcly-Taxel
Cf. #4027
0c60938
@Parcly-Taxel Parcly-Taxel mentioned this pull request Jun 5, 2023
Closed
bors bot pushed a commit that referenced this pull request Jun 5, 2023
@Parcly-Taxel
feat: mark Data.Nat.SqrtNormNum as ported (#4678)
267eb59 
Cf. #4027 and #4253.
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@kmill @qawbecrdtey
port: Nat.sqrt extension for norm_num (leanprover-community#4027)
c104967
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@Parcly-Taxel @qawbecrdtey
feat: mark Data.Nat.SqrtNormNum as ported (leanprover-community#4678)
3d6944a 
Cf. leanprover-community#4027 and leanprover-community#4253.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@kmill @semorrison @digama0