Henrik Böving

We want the `bv_decide` tactic to be able to solve things at the expressiveness of QF_BV (https://smt-lib.org/theories-FixedSizeBitVectors.shtml). This requires adding a lot of primitive operations to the bitblaster still. It...

`termination_by?` over generalizes the decreasing term

1

### 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...

RFC: indicator for out of date infoview

2

### Proposal Show some form of indicator for when the goal state that's currently being presented in the info view is out of date / being recomputed. - **User Experience**:...

`sat_decide` used to have an optimization such that it would only generate a proof term during reflection if the terms where not already defeq. This can enable a drastic reuse...

Recursive theorems with `cases` vs `match`

3

### 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...

perf: add a bitblasting cache for bv_decide's boolean substructure

3

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...

``` ; generated by nunchaku (declare-sort a 0) (declare-fun P ((=> a a)) Bool) (declare-fun swap (a) a) (assert (forall ((x a)) (not (= (swap x) x)))) (assert-not (or (P...