Skip to content

Commit

Permalink
fix parentheses
Browse files Browse the repository at this point in the history
  • Loading branch information
luisacicolini committed Oct 1, 2024
1 parent 413d92b commit 3898e69
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,7 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
simp [toInt_eq_toNat_cond]; omega

theorem eq_zero_or_eq_one {a : BitVec 1} : a = 0#1 ∨ a = 1#1 := by
theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
obtain ⟨a, ha⟩ := a
simp only [Nat.reducePow]
have acases : a = 0 ∨ a = 1 := by omega
Expand Down

0 comments on commit 3898e69

Please sign in to comment.