lean4-htt/src/Std/Tactic
Leonardo de Moura 33b45132a4
feat: bv_decide hint (#7009)
This PR ensures users get an error message saying which module to import
when they try to use `bv_decide`.
2025-02-09 17:11:28 +00:00
..
BVDecide feat: bv_decide hint (#7009) 2025-02-09 17:11:28 +00:00
BVDecide.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00