chore: add the lean4 extension to the vscode workspace (#3059)

This prompts users opening the workspace (on a new device) for the first
time to install the lean extension

# Summary

Link to `RFC` or `bug` issue: N/A
This commit is contained in:
Eric Wieser 2023-12-14 08:58:21 +00:00 committed by GitHub
parent f208d7b50f
commit d279a4871f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -48,5 +48,10 @@
}
}
]
},
"extensions": {
"recommendations": [
"leanprover.lean4"
]
}
}