Closed mhuisi closed 1 month ago
This should hopefully make it easier to find the Lean 4 extension when searching for "Lean" (due to the way that the VS Code fuzzy search works). This PR also adds a "lean4" keyword so that the extension can still be found with the old identifier.
This should hopefully make it easier to find the Lean 4 extension when searching for "Lean" (due to the way that the VS Code fuzzy search works). This PR also adds a "lean4" keyword so that the extension can still be found with the old identifier.