> So you could presumably also set it up to implement its suggestions (i.e. if it "executes" its proposed definition for `succ` that would actually just update it in the global namespace). Fun stuff.

Yep, I've had that working in some earlier version of the tooling.

> I'd suggest rethinking this; people usually expect the tab key to auto-complete.

That's a fair point.

> At any rate, thanks for writing the description yourself.

I might let an LLM write the code, and even the user's manual, but I write my own blog post and comments. :-)