From 7d7cd1a7c91f1372479a33639bfed138946b49ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Feb 2020 10:52:12 -0800 Subject: [PATCH] doc: document issue cc @dselsam --- tests/elabissues/error_aux_decl_exists.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/elabissues/error_aux_decl_exists.lean b/tests/elabissues/error_aux_decl_exists.lean index b5ab9ad88d..5a013ac950 100644 --- a/tests/elabissues/error_aux_decl_exists.lean +++ b/tests/elabissues/error_aux_decl_exists.lean @@ -17,3 +17,7 @@ def foo : Nat → Unit -- error: equation compiler failed to create auxiliary declaration 'foo._main' -- nested exception message: -- invalid declaration, a declaration named 'foo._main' has already been declared + +/- +[Leo]: Rob Lewis reported the issue for Lean3 a few years ago. I told him I would not fix it since I think it is obvious to understand the problem. We will write a new equation compiler. We will fix it if it only if it doesn't increase the complexity. +-/