Zulip Chat Archive

Stream: general

Topic: Newly Downloaded


view this post on Zulip Sean G McCain (Oct 31 2018 at 21:38):

I am using LEAN for a discrete math class. I just downloaded it for a project. Is there anything that I need to also download or is using the LEAN extension in Visual Studio all I need to get going?

view this post on Zulip Andrew Ashworth (Oct 31 2018 at 21:47):

nope, the lean extension + lean is all you need to start hacking around

view this post on Zulip Chris Hughes (Oct 31 2018 at 21:47):

This should help https://www.youtube.com/watch?v=2f_9Zetekd8

view this post on Zulip Sean G McCain (Oct 31 2018 at 21:49):

I have a Mac. Is that going to change anything?

view this post on Zulip Chris Hughes (Oct 31 2018 at 22:08):

I think there's another video on macs.

view this post on Zulip Chris Hughes (Oct 31 2018 at 22:08):

Look at Scott's channel

view this post on Zulip Kevin Buzzard (Oct 31 2018 at 22:40):

https://www.youtube.com/watch?v=k8U6YOK7c0M&t=7s is the mac one. If you are only doing super-basic maths then core Lean might have what you need, but the moment you want something like the binomial theorem you're going to need the maths library.


Last updated: May 12 2021 at 23:13 UTC