You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Mathlib has .docker and .devcontainer folders that (for one thing) make it easy to quickly load in to a fresh install of lean + mathlib (eg with gitpod.io). I think adding these to Std would be helpful
The text was updated successfully, but these errors were encountered:
Note that we're hoping to distribute Std directly with Lean itself (i.e. no require std required for projects that use it), but I think these integrations would remain just as useful even if we can pull that off.
Mathlib has
.docker
and.devcontainer
folders that (for one thing) make it easy to quickly load in to a fresh install of lean + mathlib (eg with gitpod.io). I think adding these to Std would be helpfulThe text was updated successfully, but these errors were encountered: