lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
We implement `toInt_abs`. A subtle wrinkle is to note that `abs (intMin w) = intMin w`, which complicates our proof. Furthermore, toward this proof, we add an alternative to `msb_eq_decide`...
### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...
### Proposal Currently, `throw "error" : IO A` does not typecheck. I would like it to typecheck. Reasoning: - As a seasoned Lean programmer it is still hard for me...
Small UX/documentation issue: Hovering over `simp!` tells me how `simp` works, but not what `simp!` does. ### Versions leanprover/lean4:nightly-2024-09-17 ### Impact Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others...
### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...
### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...
### Prerequisites Please put an X between the brackets as you perform the following steps: * [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [X] Reduce the...
This is a meta-issue that I’ll use to track my progress in creating a toolkit for faster kernel reduction. This is to help me organize the work, but also to...
When experimenting with encoding set as bitvectors as `Nat`s, which seems like it should be rather efficient, I noticed that processing the file in VSCode was quick enough, but `lake...
Fixes #5614
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover