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 1c2db93 commit cf9e141Copy full SHA for cf9e141
src/Lean/Meta/Constructions/NoConfusion.lean
@@ -338,7 +338,7 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
338
setReducibleAttribute name
339
let arity := ctorInfo.numParams + 1 + 2 * ctorInfo.numFields + indVal.numIndices + 1
340
let fields := kType.getNumHeadForalls
341
- modifyEnv fun env => markNoConfusion env declName (.perCtor arity fields)
+ modifyEnv fun env => markNoConfusion env name (.perCtor arity fields)
342
343
344
def mkNoConfusionCore (declName : Name) : MetaM Unit := do
0 commit comments