offer curated suggestions for "Download project" (beyond the current Mathlib suggestion)

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant

Apache License 2.0

158 stars 48 forks source link

offer curated suggestions for "Download project" (beyond the current Mathlib suggestion) #506

Closed kim-em closed 2 months ago

kim-em commented 2 months ago

Currently "Download project" comes with a default suggestion of Mathlib. (Great!)

Is it possible to change the user interface here so we give users a short list of suggestions (e.g. Mathlib + MIL + FPIL)? This would cover most new user experiences.