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

[Merged by Bors] - chore(src/linear_algebra/free_module): rename file to free_module_pid #7805

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(src/linear_algebra/free_module): rename file to free_module_pid #7805

wants to merge 3 commits into from

Conversation

riccardobrasca
Copy link
Member

In preparation for #7801

Open in Gitpod

@riccardobrasca riccardobrasca added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Jun 2, 2021
@riccardobrasca riccardobrasca mentioned this pull request Jun 2, 2021
Closed
@eric-wieser
Copy link
Member

Can you update the docstring in the moved file to explain what pid stands for?

@riccardobrasca
Copy link
Member Author

Let me know if this is not clear enough :)

@eric-wieser
Copy link
Member

Looks ok to me, possibly worth referencing the lean spelling of PID if there is one. I'll leave this to @Vierkantor who wrote the original docstring.

Vierkantor
Vierkantor approved these changes Jun 3, 2021
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Good idea, the contents of the file diverged quite a bit from how I originally envisioned them when I named it. How does this docstring sound?

bors d+

@bors
Copy link

bors bot commented Jun 3, 2021

✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jun 3, 2021
@riccardobrasca @Vierkantor
Update src/linear_algebra/free_module_pid.lean
fae6fc5 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@riccardobrasca
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Jun 3, 2021
@riccardobrasca
chore(src/linear_algebra/free_module): rename file to free_module_pid (…
2a93644 
…#7805)

In preparation for #7801
@bors
Copy link

bors bot commented Jun 3, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(src/linear_algebra/free_module): rename file to free_module_pid [Merged by Bors] - chore(src/linear_algebra/free_module): rename file to free_module_pid Jun 3, 2021
@bors bors bot closed this Jun 3, 2021
@bors bors bot deleted the rename_free_mod branch June 3, 2021 16:15
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. easy < 20s of review time. See the lifecycle page for guidelines.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@riccardobrasca @eric-wieser @Vierkantor