lean4-htt/src/Std/Tactic
Henrik Böving 297be24c0d
feat: bv_decide rewrites around ult, signExtend and extractLsb (#7480)
This PR adds the necessary rewrites for the Bitwuzla rules
BV_ULT_SPECIAL_CONST, BV_SIGN_EXTEND_ELIM, TODO.
2025-03-14 09:55:44 +00:00
..
BVDecide feat: bv_decide rewrites around ult, signExtend and extractLsb (#7480) 2025-03-14 09:55:44 +00:00
BVDecide.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00