From 2e3d52333241e01dfd09fd921cb0e26fb61fd145 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Fri, 12 Apr 2024 07:09:46 +0200 Subject: [PATCH] chore: protect Std.BitVec (#3884) This makes `Std.BitVec` a protected abbreviation so `open Std` doesn't result in ambiguity errors. --- src/Init/Data/BitVec/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 04f596ed38..68066e8af6 100644 --- 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