chore: missing instances (#4479)

cc @shigoel
2024-06-17 22:14:00 +02:00 · 2024-06-17 22:14:00 +02:00 · 06731f99d4
commit 06731f99d4
parent 59a09fb4e7
2 changed files with 2 additions and 0 deletions
--- 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
--- 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