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

chore: typo fix in error message of overlapping structure fields

Browse source
This commit is contained in:
Alex J Best 2022-11-05 14:58:51 +01:00 • committed by Gabriel Ebner
parent 999b61007c
commit 8da48f2381
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/StructInst.lean
View file

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

2
tests/lean/structInst1.lean.expected.out
View file

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