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