From dcb974a1cfa4c39e2018064f4c310a42dd4e1c9d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 May 2022 14:08:40 -0700 Subject: [PATCH] chore: remove unused parameter --- src/Lean/Elab/Structure.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index c7c8d842d3..1c0f1e5265 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -277,10 +277,13 @@ private partial def getNestedProjectionArg (e : Expr) : MetaM Expr := do return ← getNestedProjectionArg e.appArg! return e -/-- Get field type of `fieldName` in `parentStructName`, but replace references +/-- + Get field type of `fieldName` in `parentType`, but replace references to other fields of that structure by existing field fvars. - Auxiliary method for `copyNewFieldsFrom`. -/ -private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Name) (parentType : Expr) (fieldName : Name) : MetaM Expr := do + Auxiliary method for `copyNewFieldsFrom`. + +-/ +private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fieldName : Name) : MetaM Expr := do withLocalDeclD (← mkFreshId) parentType fun parent => do let proj ← mkProjection parent fieldName let projType ← inferType proj @@ -393,7 +396,7 @@ where let rec copy (i : Nat) (infos : Array StructFieldInfo) (fieldMap : FieldMap) (expandedStructNames : NameSet) : TermElabM α := do if h : i < fieldNames.size then let fieldName := fieldNames.get ⟨i, h⟩ - let fieldType ← getFieldType infos parentStructName parentType fieldName + let fieldType ← getFieldType infos parentType fieldName match findFieldInfo? infos fieldName with | some existingFieldInfo => let existingFieldType ← inferType existingFieldInfo.fvar