fix: use Expr.equal instead of Expr.eqv

`Expr.equal` takes binder names into account.
leanprover · Nov 16, 2024 · 8be8441 · 8be8441
1 parent 1d3f02e
commit 8be8441
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
@@ -335,7 +335,12 @@ structure ExprConfigCacheKey where
   private mk ::
   expr      : Expr
   configKey : UInt64
-  deriving Inhabited, BEq
+  deriving Inhabited
+
+instance : BEq ExprConfigCacheKey where
+  beq a b :=
+    Expr.equal a.expr b.expr &&
+    a.configKey == b.configKey
 
 instance : Hashable ExprConfigCacheKey where
   hash := fun { expr, configKey } => mixHash (hash expr) (hash configKey)