perf: use hasExprMvar in type class search

leanprover · May 25, 2024 · b8de322 · b8de322
1 parent b0c1112
commit b8de322
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
@@ -248,7 +248,7 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
     let mctx ← getMCtx
     return some {
       mvar, key, mctx, instances
-      typeHasMVars := mvarType.hasMVar
+      typeHasMVars := mvarType.hasExprMVar
       currInstanceIdx := instances.size
     }