chore: protect Std.BitVec

2026-03-18 02:44:12 +00:00 · 2024-04-12 06:54:15 +02:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -34,7 +34,7 @@ structure BitVec (w : Nat) where
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (2^w)

-@[deprecated] abbrev Std.BitVec := _root_.BitVec
+@[deprecated] protected abbrev Std.BitVec := _root_.BitVec

 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we