leanproject integration

Open bryangingechen opened this issue 5 years ago • 0 comments

Is there a way to have the extension run leanproject get-mathlib-cache or leanproject get-cache if we "obviously" need to?

Oct 22 '20 23:10 bryangingechen