feat: add BitVec.toNat_[udiv|umod] and [udiv|umod]_eq #15
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
Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves the identifier when expanding the macro, saving needing to use the fully qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`, throws an error if the identifier cannot be resolved. Closes leanprover#4899
This is a better fix to the problem reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nat.20fighting, which itself had a problem as reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression/near/456539091.
.. as well as neg_neq_iff_neq_neg. --------- Co-authored-by: Henrik Böving <hargonix@gmail.com>
We observed a small performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean Before: 2.65s After: 2.60s
Closes leanprover#4513 --------- Co-authored-by: Kim Morrison <kim@tqft.net>
After having added already `BitVec.ushiftRight_*_distrib`in leanprover#4667 for ushiftRight, this PR now completes the `*_distrib` theorems for shift.
Helpful for diagnosing which linter is failing, c.f. [recent problem](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/quote4/near/457349304) in quote4.
Co-authored-by: Siddharth <siddu.druid@gmail.com>
tobiasgrosser
force-pushed
the
bitvec_udiv_umod_basics
branch
from
23a2884
to
01a2342
Compare
Without this change, a stack overflow on Mac OS during tactic execution
can lead to the message:
terminated by signal SIGBUS (Misaligned address error)
This comes from `lean_alloc_small`. With the change, the process instead
terminates with the more accurate and actionable:
Stack overflow detected. Aborting.
The prior default of 1000000 could not be achieved in practice, because the stack would overflow after around 5000 recursive invocations. This meant that a poorly-chosen @[ext] lemma could crash Lean. Talking to Mathlib users, it seems that 10 would be a very large number in practice, so a default limit of 100 should not change successful uses. But it does make it much easier to diagnose and recover from poor choices of @[ext] lemmas.
Co-authored-by: Atticus Kuhn <52258164+AtticusKuhn@users.noreply.github.com>
...unless we are about to kill the process anyway (which is not the default) Ensures panics are visible as regular messages in the language server and properly ordered in relation to other messages on the cmdline
Step 2/~7 in upstreaming LeanSAT. --------- Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Siddharth <siddu.druid@gmail.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
According to the release notes of cache this should not break anything as they merely upgraded the node version.
…over#4982) For structure projections, the pretty printer assumed that the expression was type correct. Now it checks that the object being projected is of the correct type. Such terms appear in type mismatch errors. Also, fixes and improves `#print` for structures. The types of projections now use MessageData (so are now hoverable), and the type of `self` is now the correct type. Closes leanprover#4670
…5004) leanprover#4976 moved resolution of a promise to an earlier point, but that led to object being marked MT earlier, so we need to move the code that minimizes those objects earlier too to revert the performance regression.
…anprover#5012) as that’s the simp normal form.
|
This has been merged in leanprover@7c5d866 |
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.
Co-authored-by: Siddharth siddu.druid@gmail.com