lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
The current `Classical.em` proof isn't that easy to follow. Since Lean has quotients, we can take a two-element type like `Bool`, and quotient it by `x = y ∨ P`....
This fixes indentation before `|` in places where the amount of spaces was not 0 or 2. I suppose this is the non-controversial part of #2580. Deciding for either 0...
Fixes #2483
* [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/memory.20model.20of.20natural.20numbers/near/387485542) Documentation regarding the borrowing convention of arguments and return values for C functions in `lean.h` and related files is very important for FFI writers to be able...
implementation based on: https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=987767 co-authored by @bollu
This PR adds a small docstring to `Simp.Methods.discharge?` - (this is what I *think* it does, so any corrections are appreciated:)) This was suggested in the review of [this mathlib...
This PR provides functions to merge and split vectors of bitvectors, taking up the abandoned #3727.
This PR ensures that `libuv` objects are cleaned up by `finalize_runtime_module()`. Closes #7753
This PR adds a bitblasting cache for the boolean substructure of problems that bv_decide works on in addition to the one used for bvexpr. Unfortunately this is currently causing a...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover