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.
+-/