Lean register_label_attr not working

Stream: general

[Frederick Pu]

Can someone explain to me why this is not working. I'm really new to register_labell_attr:

import Lean.LabelAttribute

/-
  test label
-/
register_label_attr rom

@[rom] -- unknown attribute rom
def womp : 2 + 2 = 4 := by rfl

[Damiano Testa]

I think that you cannot define and use an attribute in the same file: the file where the attribute is used should import the file where the attribute is registered.

If you move

@[rom] -- unknown attribute rom
def womp : 2 + 2 = 4 := by rfl

to a separate file importing the previous one, it should work.

[Asei Inoue]

very interesting.
why Lean forbids to define attribute and use it in same file

[Asei Inoue]

I think it is very inconvenient…

[Asei Inoue]

For example, register_label_attr doesn’t work in Lean4 web.

[Asei Inoue]

Even if there is reasonable reason, the error message should suggest file separation.

[Kim Morrison]

Could you open an issue about the error message?

[Asei Inoue]

@Kim Morrison done! https://github.com/leanprover/lean4/issues/4011

[Asei Inoue]

Why can't we register and use label in the same file?