lean4-htt/src/Std/Tactic/BVDecide
2024-09-10 15:24:23 +10:00
..
Bitblast refactor: make extractLsb' the primitive bv_decide understands, rather than extractLsb (#5211) 2024-09-04 08:02:04 +00:00
LRAT chore: rename Array.data to Array.toList 2024-09-10 15:24:23 +10:00
Normalize refactor: make extractLsb' the primitive bv_decide understands, rather than extractLsb (#5211) 2024-09-04 08:02:04 +00:00
Bitblast.lean
LRAT.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00
Normalize.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00
Reflect.lean refactor: make extractLsb' the primitive bv_decide understands, rather than extractLsb (#5211) 2024-09-04 08:02:04 +00:00
Syntax.lean feat: import LeanSAT's tactic frontends 2024-08-28 18:14:39 +02:00