The problem is that `auto_param` is defined in the old `init/meta/name` module, and we don't want to have `init/meta` dependencies in the `init/lean` modules. |
||
|---|---|---|
| .. | ||
| ir | ||
| parser | ||
| format.lean | ||
| name.lean | ||
The problem is that `auto_param` is defined in the old `init/meta/name` module, and we don't want to have `init/meta` dependencies in the `init/lean` modules. |
||
|---|---|---|
| .. | ||
| ir | ||
| parser | ||
| format.lean | ||
| name.lean | ||