From 13721cdfe9059d8af0040396d05ba1b191a43658 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 13 Feb 2020 10:25:10 -0800 Subject: [PATCH] doc: elabissue for structure same-name error msg --- tests/elabissues/structure_same_names2.lean | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 tests/elabissues/structure_same_names2.lean 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'