mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
24 lines
779 B
Lean4
24 lines
779 B
Lean4
/-
|
|
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
|
|
|
|
/-
|
|
[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.
|
|
-/
|