From 94e45f7b819fbc756d2c0b22d571289b872e65f8 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 13 Feb 2020 16:23:28 -0800 Subject: [PATCH] doc: elabissue for '_main already defined' msg --- tests/elabissues/error_aux_decl_exists.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/elabissues/error_aux_decl_exists.lean diff --git a/tests/elabissues/error_aux_decl_exists.lean b/tests/elabissues/error_aux_decl_exists.lean new file mode 100644 index 0000000000..b5ab9ad88d --- /dev/null +++ b/tests/elabissues/error_aux_decl_exists.lean @@ -0,0 +1,19 @@ +/- +Sub-optimal error message. +The implementation detail that an auxiliary function `foo._main` leaks, +when there is a simple explanation for the problem that doesn't involve it. +-/ + +def foo : Nat → Unit +| 0 => () +| n+1 => foo n + +-- Second recursive function with same name. +/- +def foo : Nat → Unit +| 0 => () +| n+1 => foo n +-/ +-- error: equation compiler failed to create auxiliary declaration 'foo._main' +-- nested exception message: +-- invalid declaration, a declaration named 'foo._main' has already been declared