refactor: consistently use variable w for the width of a bitvector
#646
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
Additionally, drop `{w}` implicit arguments in favor of a `variable {w : Nat}` at the start of the file.
This has one functional change:
the type of `getLsb_cons` used to be `(b : Bool) -> {w : Nat} -> ...`, but is now `{w : Nat} -> (b : Bool)`.
|
WIP |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
merge-conflict
|
If there's still useful material here, it will need to be moved to the Lean repo, and BitVec/Lemmas has been upstreamed. |
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.
Currently, lemmas about bitvectors inconsistently use
n, m, vandwfor the width.I've (arbitrarily) picked
was the blessed variable, and changed all lemmas to use this, only usingvwhen a lemma involves two bitvectors of differing widths.I don't think the exact choice of variable matters much, but it does matter that we pick one and consistently use it.
This changes only the name of variables, it should not break any other code.
Additionally, I've dropped
{w}implicit arguments in favor of avariable {w : Nat}at the start of the file.This has one functional change: the type of
getLsb_consused to be(b : Bool) -> {w : Nat} -> ..., but is now{w : Nat} -> (b : Bool). Since this only changes the order of an implicit argument, the impact of this change should be very small.This is still a work-in-progress. I've opened the PR already as a draft to see if I can get a leaff report to confirm there are no functional changes besides the one described above