From 3896c44b557ba67168c16e996ceec369fd47bd05 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Aug 2021 10:49:06 -0700 Subject: [PATCH] chore: fix incorrect comment Signed-off-by: Leonardo de Moura --- src/Lean/Elab/Structure.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index eb245754a6..fee7ee5b90 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -63,7 +63,7 @@ inductive StructFieldKind where structure StructFieldInfo where name : Name - declName : Name -- Remark: this field value doesn't matter for fromParent fields. + declName : Name -- Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary `_default` functions. fvar : Expr kind : StructFieldKind inferMod : Bool := false