lean4-htt/src/Std/Tactic
Henrik Böving 837a67bedb
feat: change bv_decide to an elaborated config (#6010)
This PR changes `bv_decide`'s configuration from lots of `set_option` to
an elaborated config like `simp` or `omega`. The notable exception is
`sat.solver` which is still a `set_option` such that users can configure
a custom SAT solver globally for an entire project or file. Additionally
it introduces the ability to set `maxSteps` for the simp preprocessing
run through the new config.

The latter feature was requested by people using `bv_decide` on SMTLIB
which has ginormous terms that exceed the default.
2024-11-08 13:15:04 +00:00
..
BVDecide feat: change bv_decide to an elaborated config (#6010) 2024-11-08 13:15:04 +00:00
BVDecide.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00