Zulip Chat Archive

Stream: general

Topic: A technical question

view this post on Zulip Ned Summers (Jul 12 2018 at 13:02):

Hey all. A more technical question, I'm working in category theory (very new to this) and I think I want to fork Scott Morrison's mathlib (https://github.com/semorrison/lean-category-theory) as hardly anything is on the regular mathlib yet. I'm using VS code on my own windows laptop but I'm really amateur with pretty much any of the technical aspect (command line and upwards) so I'm not really sure how to even begin on this. I installed Lean (nightly) and mathlib from a tutorial originally. If anyone could even just direct me to what to google/a tutorial, I'd really appreciate it.

view this post on Zulip Reid Barton (Jul 12 2018 at 13:06):

You should be able to follow the instructions at https://github.com/kbuzzard/lean-stacks-project/ with obvious adjustments

Last updated: May 09 2021 at 19:11 UTC