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.

Sign up for GitHub

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

Jump to bottom

feat: setup simp lemmas: 'msb -> getLsb -> decide ...' #3436

Merged
merged 3 commits into from
Feb 22, 2024
Merged

feat: setup simp lemmas: 'msb -> getLsb -> decide ...' #3436

merged 3 commits into from
Feb 22, 2024

Conversation

bollu
Copy link
Contributor

@bollu bollu commented Feb 21, 2024

This is a follow up to 'leanprover-community/batteries#645', where the simp lemmas were requested: leanprover-community/batteries#645 (comment)

Note that @semorrison asked to use (Fin.last _) to index. Now that we use a Nat to index msb , the pattern (Fin.last _) would not have the width be automatically inferred. Therefore, I've changed the definitions to use Nat for indexing.

@bollu
feat: setup simp lemmas: 'msb -> getLsb -> decide ...'
a6e9292 
This is a follow up to 'leanprover-community/batteries#645',
where the simp lemmas were requested.
@bollu
Copy link
Contributor Author

bollu commented Feb 21, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Feb 21, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 89490f648a6f41c3f43724a52f6ac61c6072eb4a --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-21 12:45:47)

@bollu bollu mentioned this pull request Feb 21, 2024
Open
@kim-em
Copy link
Collaborator

kim-em commented Feb 21, 2024

Oh getLsb_last is a good simp lemma, you didn't need to remove that!

I'm just going to push that back, and merge now.

@kim-em kim-em enabled auto-merge February 21, 2024 23:52
@kim-em kim-em added this pull request to the merge queue Feb 22, 2024
Merged via the queue into leanprover:master with commit b6ed97b Feb 22, 2024
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@bollu @leanprover-community-mathlib4-bot @kim-em