open private

Stream: Is there code for X?

[Eric Wieser]

I saw this mentioned in a lean4 thread - is there a way to reference or add attributes to a private definition in lean 3 + Mathlib?

[Johan Commelin]

Didn't Mario show that basically anything is possible, in one of his "hacking lean 3 syntax" threads?

[Mario Carneiro]

You can do this programmatically, by looking up the name and then calling the function that adds an attribute to a definition