Skip to content

Commit 7c9718d

Browse files
chore: de-line
Co-authored-by: Tobias Grosser <[email protected]>
1 parent 62bb66b commit 7c9718d

File tree

1 file changed

+3
-1
lines changed
  • src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations

1 file changed

+3
-1
lines changed

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,7 +109,9 @@ theorem go_denote_eq {w : Nat} (aig : AIG α)
109109
simp only [show ¬curr = 0 by omega, ↓reduceIte] at hacc
110110
by_cases hcw : curr = w
111111
· subst hcw; simp [hacc]
112-
· simp only [hacc]; rw [BitVec.clzAuxRec_eq_of_le]; omega
112+
· simp only [hacc];
113+
rw [BitVec.clzAuxRec_eq_of_le]
114+
omega
113115

114116
end blastClz
115117

0 commit comments

Comments
 (0)