Update src/Init/Data/BitVec/Lemmas.lean

opencompl · Dec 5, 2024 · a09aa3c · a09aa3c
1 parent cd4f969
commit a09aa3c
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
@@ -1771,7 +1771,7 @@ theorem toNat_append_lt {m n : Nat} (x : BitVec m) (y : BitVec n) :
     <;> omega
   · omega
 
-@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
+@[simp] theorem toFin_append {x : BitVec m} {y : BitVec n} :
     (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (toNat_append_lt x y) := by
   ext
   simp