From 19da0229a94d0d80e20e7b633a2929a372a9c17a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Jul 2020 10:20:42 -0700 Subject: [PATCH] chore: fix test --- tests/lean/struct1.lean.expected.out | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 7c6437cd94..113ad0eb72 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -2,3 +2,5 @@ struct1.lean:9:14: error: expected Type struct1.lean:12:20: error: expected structure struct1.lean:15:27: error: field 'toA' has already been declared struct1.lean:18:27: error: field 'x' from 'B' has already been declared +struct1.lean:22:1: error: invalid field name '_x', identifiers starting with '_' are reserved to the system +struct1.lean:25:3: error: invalid field name '_y', identifiers starting with '_' are reserved to the system