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

fix: cond reflection bug in bv_decide (#6517)

Browse source 
This PR fixes a slight bug that was created in the reflection of `bif`
in `bv_decide`.

Tagged as changelog-no as the code in question isn't in an RC yet.
This commit is contained in:
Henrik Böving 2025-01-03 20:35:58 +01:00 • committed by GitHub
parent 7b496bf44b
commit 58d178e68f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Std/Tactic/BVDecide/Reflect.lean
View file

@ -156,7 +156,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
theorem cond_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
(h3 : rhs' = rhs) :
(bif discr' = true then lhs' else rhs') = (bif discr = true then lhs else rhs) := by
(bif discr' then lhs' else rhs') = (bif discr then lhs else rhs) := by
simp[*]
theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by