feat: suggest qualified names while editing Verso docstrings#10584

david-christiansen merged 3 commits intoleanprover:masterleanprover/lean4:masterfrom

david-christiansen:name-out-of-scope-suggestiondavid-christiansen/lean4:name-out-of-scope-suggestionCopy head branch name to clipboard