Using new attribute in the same file

Stream: lean4

[Adam Topaz]

I want to create some attribute, and for development and debugging, I would like to experiment with it in the same file. But I can't figure out how to register the attribute and have it work later on in the file. What am I missing?

import Lean

open Lean Meta in
initialize registerBuiltinAttribute {
  name := `foo
  descr := "test"
  add := fun _ _ _ ↦ do
    dbg_trace "hello world"
}

@[foo] -- error on this line
def foobar : Nat := 0

[Jireh Loreaux]

IIRC you just can't do this. You need to register the attribute in a separate file and import it.

[Adam Topaz]

Strange. There is no command I can call in the middle somewhere that "simulates" the act of making a new file?

[Jireh Loreaux]

I think not. I could be wrong, but I think the reason has something to do with it being rather expensive to initialize the environment. I'm obviously not well-versed in this though.