Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/nat/prime): norm_num plugin for factors#8009

Closed
digama0 wants to merge 2 commits intomasterfrom
norm_num_factors
Closed

[Merged by Bors] - feat(data/nat/prime): norm_num plugin for factors#8009
digama0 wants to merge 2 commits intomasterfrom
norm_num_factors

Conversation

@digama0
Copy link
Copy Markdown
Member

@digama0 digama0 commented Jun 20, 2021

Implements a norm_num plugin to evaluate terms like nat.factors 231 = [3, 7, 11].

@bryangingechen
Copy link
Copy Markdown
Collaborator

Should this be mentioned in the norm_num tactic doc entry?

@bryangingechen bryangingechen added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Jun 22, 2021
@gebner
Copy link
Copy Markdown
Member

gebner commented Jun 24, 2021

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 24, 2021
bors bot pushed a commit that referenced this pull request Jun 24, 2021
Implements a `norm_num` plugin to evaluate terms like `nat.factors 231 = [3, 7, 11]`.
@bors
Copy link
Copy Markdown

bors bot commented Jun 24, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/nat/prime): norm_num plugin for factors [Merged by Bors] - feat(data/nat/prime): norm_num plugin for factors Jun 24, 2021
@bors bors bot closed this Jun 24, 2021
@bors bors bot deleted the norm_num_factors branch June 24, 2021 11:32
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-meta Tactics, attributes or user commands

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants