Command auto-completion

Stream: lean4

[Patrick Massot]

@Marc Huisinga since you seem to be in an auto-complete mood after this glorious lean4#7134, would it be possible to get auto-complete for commands? For instance typing theo and asking for auto-complete would propose theorem.

[Marc Huisinga]

I'm not quite in an auto-completion mood anymore because I have to work on other things, but it's on my to-do list for the next time I touch auto-completion :-)