diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 1040c0e715..1525124cd9 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -410,14 +410,15 @@ where | none => let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable! let addNewField : TermElabM α := do - let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do + let fieldMap := fieldMap.insert fieldName fieldFVar + let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName let fieldDeclName := structDeclName ++ fieldName let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName addDocString' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn) let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?, kind := StructFieldKind.copiedField } - copy (i+1) infos (fieldMap.insert fieldName fieldFVar) expandedStructNames + copy (i+1) infos fieldMap expandedStructNames if fieldInfo.subobject?.isSome then let fieldParentStructName ← getStructureName fieldType if (← findExistingField? infos fieldParentStructName).isSome then diff --git a/tests/lean/2178.lean b/tests/lean/2178.lean new file mode 100644 index 0000000000..0d6d253690 --- /dev/null +++ b/tests/lean/2178.lean @@ -0,0 +1,10 @@ +class Zero (α : Type u) where + zero : α +class AddZeroClass (M : Type u) extends Zero M, Add M +class AddMonoid (M : Type u) extends AddZeroClass M where + nsmul : Nat → M → M := fun _ _ => Zero.zero +class AddCommMonoid (M : Type u) extends Zero M, AddMonoid M +class AddMonoidWithOne (R : Type u) extends AddMonoid R +class AddCommMonoidWithOne (R : Type u) extends AddMonoidWithOne R, AddCommMonoid R +class NonAssocSemiring (α : Type u) extends Zero α, AddCommMonoidWithOne α +class Semiring (α : Type u) extends Zero α, NonAssocSemiring α diff --git a/tests/lean/2178.lean.expected.out b/tests/lean/2178.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2