From 58d178e68f47897ed804000be7abbd27cf389d4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 3 Jan 2025 20:35:58 +0100 Subject: [PATCH] fix: cond reflection bug in bv_decide (#6517) 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. --- src/Std/Tactic/BVDecide/Reflect.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean index 8925371547..070d10aa9f 100644 --- a/src/Std/Tactic/BVDecide/Reflect.lean +++ b/src/Std/Tactic/BVDecide/Reflect.lean @@ -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