defining attributes

Stream: lean4

[Moritz Doll]

Hi,
according to lean4/tests/pkg/user_attr/UserAttr/Tst.lean the simple way to define attributes is TagAttribute ← registerTagAttribute, but the simple

import Lean

open Lean

initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"

@[bla] def test (a : ℕ) := a

fails with unknown attribute [bla]. Any ideas why this does not work?

[Jannis Limperg]

initialize has no effect in the file where you use it. Once you import this file somewhere else, the initialize takes effect.

[Moritz Doll]

ok, thanks