Zulip Chat Archive

Stream: lean4

Topic: Porting Mathlib: Style Changes


view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 19:04):

Lean 4 introduces various new features that may make mathlib cleaner. We should use these features only after getting mathlib as a whole to compile.

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:30):

This thread seems no longer necessary as it has been discussed on other threads.

view this post on Zulip Bryan Gin-ge Chen (Jan 10 2021 at 03:31):

Do you mind linking to those threads so folks stumbling on this one in the future will be able to find them?

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:34):

I will link to the specific messages inside those threads, in case the threads are too long

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:37):

Mario Carneiro said:

I don't think it will be a big deal to switch to by. There is no need to preserve syntax this much, particularly if we're going to be doing the port based on an initial syntax transformation of mathlib to lean 4 style

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:38):

Mario Carneiro said:

I do think it's worth it to keep Type* and Sort* though, which as I mentioned in another thread can be added to the mathlib prelude

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:40):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/capitalization

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:42):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/what.20naming.20scheme.20to.20use.20in.20mathlib4

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:43):

Threads that are short enough and almost entirely about style can be simply linked to

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:49):

(deleted)

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:50):

(deleted)

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:53):

For this thread, I will try to quote key messages about style. How I choose those messages might be biased though, so it might still be a good idea for anyone reading this thread to visit the threads where those messages where from.

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:55):

(deleted)

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 03:56):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Jan 10 2021 at 03:58):

If the idea is to close off discussion in this thread, I think linking just once to each related previous thread is fine.

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 04:00):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lemma

view this post on Zulip Mohamed Al-Fahim (Jan 10 2021 at 04:00):

Bryan Gin-ge Chen said:

If the idea is to close off discussion in this thread, I think linking just once to each related previous thread is fine.

True. I am starting to feel bad from quoting some messages out of context :sweat_smile:


Last updated: May 18 2021 at 23:14 UTC