From 0fb936158bcf605268cd7e735bbda8b7794a1cd9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 21 Feb 2024 05:37:00 -0800
Subject: [PATCH] chore: explicit `DecidableEq` instance for `BitVec` (#3438)

---
 src/Init/Data/BitVec/Basic.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 74adceacbb..b1d529c4f7 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -33,7 +33,19 @@ structure BitVec (w : Nat) where
   /-- Interpret a bitvector as a number less than `2^w`.
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
-  deriving DecidableEq
+
+-- We manually derive the `DecidableEq` instances for `BitVec` because
+-- we want to have builtin support for bit-vector literals, and we
+-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
+def BitVec.decEq (a b : BitVec n) : Decidable (a = b) :=
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ =>
+    if h : n = m then
+      isTrue (h ▸ rfl)
+    else
+      isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
+
+instance : DecidableEq (BitVec n) := BitVec.decEq
 
 namespace BitVec