Non-builtin parser aliases

Stream: lean4

[Mario Carneiro]

Is it possible to declare a parser alias like withoutPosition(p) in user code? I get an error aliases can only be registered during initialization which I think means I need to use builtin_initialize, but if I do then it appears to have no effect.

[Sebastian Ullrich]

I don't think anyone tried or even thought about that yet. initialize doesn't work?

[Mario Carneiro]

it doesn't

[Mario Carneiro]

also, apparently there is both IO.initializing and initializing and they aren't the same thing

[Mario Carneiro]

haha lol if I just delete the error message then it works