From e8403f89b05d78a960d367c31c7e4a3e648b3d50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Aug 2021 16:02:33 -0700 Subject: [PATCH] fix: ensure field names are atomic --- src/Lean/Elab/Structure.lean | 4 +++- tests/lean/nonAtomicFieldName.lean | 2 ++ tests/lean/nonAtomicFieldName.lean.expected.out | 1 + 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/nonAtomicFieldName.lean create mode 100644 tests/lean/nonAtomicFieldName.lean.expected.out diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index e1074980ed..84efdfc927 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -207,7 +207,9 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str pure (some optBinderTacticDefault[0][1]) let idents := fieldBinder[2].getArgs idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do - let name := ident.getId + let name := ident.getId.eraseMacroScopes + unless name.isAtomic do + throwErrorAt ident "invalid field name '{name.eraseMacroScopes}', field names must be atomic" let declName := structDeclName ++ name let declName ← applyVisibility fieldModifiers.visibility declName addDocString' declName fieldModifiers.docString? diff --git a/tests/lean/nonAtomicFieldName.lean b/tests/lean/nonAtomicFieldName.lean new file mode 100644 index 0000000000..afe031250b --- /dev/null +++ b/tests/lean/nonAtomicFieldName.lean @@ -0,0 +1,2 @@ +structure A where + a.b : Nat diff --git a/tests/lean/nonAtomicFieldName.lean.expected.out b/tests/lean/nonAtomicFieldName.lean.expected.out new file mode 100644 index 0000000000..872b554274 --- /dev/null +++ b/tests/lean/nonAtomicFieldName.lean.expected.out @@ -0,0 +1 @@ +nonAtomicFieldName.lean:2:2-2:5: error: invalid field name 'a.b', field names must be atomic