max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: bv_normalize handle -> False (#5507)

Browse source
This commit is contained in:
Henrik Böving 2024-09-28 12:05:16 +02:00 • committed by GitHub
parent 16a16898d5
commit 5f22ba7789
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Std/Tactic/BVDecide/Normalize/Prop.lean
View file

@ -30,6 +30,7 @@ attribute [bv_normalize] true_iff
attribute [bv_normalize] iff_false
attribute [bv_normalize] false_iff
attribute [bv_normalize] false_implies
attribute [bv_normalize] imp_false
attribute [bv_normalize] implies_true
attribute [bv_normalize] true_implies
attribute [bv_normalize] not_true

3
tests/lean/run/bv_decide_rewriter.lean
View file

@ -13,3 +13,6 @@ example (z : BitVec 64) : True := by
example :
¬ (0 ≤ 0 + 16#64 ∧ 0 ≤ 0 + 16#64 ∧ (0 + 16#64 ≤ 0 ∨ 0 ≥ 0 + 16#64 ∨ 16#64 = 0 ∨ 16#64 = 0)) := by
bv_normalize
example (x y z : BitVec 8) (h1 : x = z → False) (h2 : x = y) (h3 : y = z) : False := by
bv_decide