chore: implicit args

Co-authored-by: Siddharth <[email protected]>
opencompl · Feb 20, 2025 · 0a4678b · 0a4678b
1 parent 701c47b
commit 0a4678b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,7 +781,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by
   simp [extractLsb, toInt_ofNat]
 
-@[simp] theorem extractLsb'_toFin (s m : Nat) (x : BitVec n) :
+@[simp] theorem extractLsb'_toFin {s m : Nat} {x : BitVec n} :
     (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by
   simp [extractLsb', toInt_ofNat]