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

Small cleanup #358

Merged
merged 1 commit into from
Mar 26, 2021
Merged

Small cleanup #358

merged 1 commit into from
Mar 26, 2021

Conversation

pi8027
Copy link
Member

@pi8027 pi8027 commented Mar 26, 2021

If the computational contents of proper_pinfty_nbhs and proper_ninfty_nbhs do not matter, these changes would be OK.

@pi8027
Copy link
Member Author

pi8027 commented Mar 26, 2021

I found myself good at this kind of refactoring work, and it also helps me to understand existing code. So I wish to have a list of lemmas I should try to refactor when I have some time.

@pi8027
Copy link
Member Author

pi8027 commented Mar 26, 2021

I replaced Defined with Qed as discussed in the meeting.

@affeldt-aist affeldt-aist self-requested a review March 26, 2021 13:47
@affeldt-aist affeldt-aist merged commit 88ac986 into math-comp:master Mar 26, 2021
@pi8027 pi8027 deleted the refactor branch March 27, 2021 08:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants