lean4-vscode search

Stream: general

[Tristan Figueroa-Reid]

Is there a way to search for abbreviations inside the find and replace menu? If not, was there any opposition to adding such a feature?

[David Thrane Christiansen]

As I understand it, this is a limitation in the VS Code extension API.