[Merged by Bors] - chore(data/fin): reorder file to group declarations #6109
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Do you mind adding some sectioning module doc strings like this while you're reorganizing things? /-!
### title
-/These will also make the web docs more readable. |
1 task
|
@pechersky, would you mind making PRs by pushing branches to the main repository? It's easier for reviewers to check out copies / merge into other branches, etc., if we don't need to configure other remotes. |
|
@semorrison It is a branch on the main repo, but it has a |
pechersky
added
the
awaiting-review
Awesome --- excellent practice! :-) |
|
bors merge |
github-actions
bot
added
ready-to-merge
1 task
bors bot
pushed a commit
that referenced
this pull request
Feb 10, 2021
The `data/fin` file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on `fin` operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added. This is useful in preparation for redefining `fin` operations (lean#527). Additionally, it allows for better organization for other refactors like making `pred` and `pred_above` total.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
b-mehta
pushed a commit
that referenced
this pull request
Apr 2, 2021
The `data/fin` file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on `fin` operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added. This is useful in preparation for redefining `fin` operations (lean#527). Additionally, it allows for better organization for other refactors like making `pred` and `pred_above` total.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The
data/finfile has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely onfinoperations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added.This is useful in preparation for redefining
finoperations (lean#527). Additionally, it allows for better organization for other refactors like makingpredandpred_abovetotal.