From 8da48f238169582f3255206cfd8755fd7a350116 Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Sat, 5 Nov 2022 14:58:51 +0100 Subject: [PATCH] chore: typo fix in error message of overlapping structure fields --- src/Lean/Elab/StructInst.lean | 2 +- tests/lean/structInst1.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 868c818f66..51cc3c1cc9 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -435,7 +435,7 @@ private def mkFieldMap (fields : Fields) : TermElabM FieldMap := match fieldMap.find? fieldName with | some (prevField::restFields) => if field.isSimple || prevField.isSimple then - throwErrorAt field.ref "field '{fieldName}' has already beed specified" + throwErrorAt field.ref "field '{fieldName}' has already been specified" else return fieldMap.insert fieldName (field::prevField::restFields) | _ => return fieldMap.insert fieldName [field] diff --git a/tests/lean/structInst1.lean.expected.out b/tests/lean/structInst1.lean.expected.out index 9903d88d86..6cd127f3e2 100644 --- a/tests/lean/structInst1.lean.expected.out +++ b/tests/lean/structInst1.lean.expected.out @@ -1,3 +1,3 @@ -structInst1.lean:12:11-12:19: error: field 'toA' has already beed specified +structInst1.lean:12:11-12:19: error: field 'toA' has already been specified f5 : C → A → C f6 : C → A → A