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.
I pulled
intMin
andintMax
up in theLemmas
file. To do so, I had to move other sections down. Most significant changes include:toNat_shiftLeft
andgetLsbD_shiftLeft
out of theshiftLeft
section, at the very beginning of the file, since these two are crucial to most of the subsequent theoremsadd_zero
andzero_add
or_allOnes
,allOnes_or
,and_allOnes
,Std.LawfulCommIdentity
,allOnes_and
,negOne_eq_allOnes
moved from their respective operator section to theallOnes
section)Overall,
intMax
andintMin
are now only preceded by sectionstwoPow
,le and lt
,mul
,sub/neg
,add
and the theorems in (1). As far as I could see, these sections are very much interdependent and therefore hard to move further around. PullingintMax
andintMin
further up would require breaking up these sections.