From 06731f99d425c3f098cd88ef08f68aa7de71eb39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 17 Jun 2024 22:14:00 +0200
Subject: [PATCH] chore: missing instances (#4479)

cc @shigoel
---
 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean | 1 +
 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean    | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
index 882f44f76b..5c78ba1b4e 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
@@ -19,6 +19,7 @@ structure Literal where
   n     : Nat
   /-- Actual value. -/
   value : BitVec n
+  deriving DecidableEq, Repr
 
 /--
 Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
index 98f65f2b43..85d3ef16db 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
@@ -14,6 +14,7 @@ open Lean Meta Simp
 structure Value where
   n     : Nat
   value : Fin n
+  deriving DecidableEq, Repr
 
 def fromExpr? (e : Expr) : SimpM (Option Value) := do
   let some ⟨n, value⟩ ← getFinValue? e | return none