diff --git a/tests/elabissues/structure_same_names2.lean b/tests/elabissues/structure_same_names2.lean new file mode 100644 index 0000000000..a3ad17d0a0 --- /dev/null +++ b/tests/elabissues/structure_same_names2.lean @@ -0,0 +1,2 @@ +-- Bad error message when same name is used as parameter and field +structure Foo (n : Nat) : Type := (n : Nat) -- error: invalid return type for 'Foo.mk'