max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unused parameter

Browse source
This commit is contained in:
Leonardo de Moura 2022-05-26 14:08:40 -07:00
parent fc606f3ab5
commit dcb974a1cf
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/Structure.lean
View file

@ -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