Delaborator for examples from lean4 manual

Stream: Is there code for X?

[Ira Fesefeldt]

Does someone maybe know where I can find a delaborator example for notation similar to the examples of the lean4 manual here?

[Kyle Miller]

I don't know, but it's a good question, and I put this on my to-do list.