We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 43171d1 commit f60cee3Copy full SHA for f60cee3
src/Lean/Meta/Match/MatchEqs.lean
@@ -482,7 +482,7 @@ where go baseName :=
482
let thmType ← unfoldNamedPattern thmType
483
let thmVal ← mkFreshExprSyntheticOpaqueMVar thmType
484
let mvarId := thmVal.mvarId!
485
- let canUseGrind := ((← getEnv).getModuleIdx? `InitGrind).isSome
+ let canUseGrind := ((← getEnv).getModuleIdx? `Init.Grind).isSome
486
if canUseGrind then -- TMP
487
proveCongrEqThm matchDeclName thmName mvarId
488
else
0 commit comments