## Stream: lean4

### Topic: Porting Mathlib: Style Changes

#### 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.

#### Mohamed Al-Fahim (Jan 10 2021 at 03:30):

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

#### 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?

#### 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

#### 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

#### 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

#### Mohamed Al-Fahim (Jan 10 2021 at 03:40):

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

#### 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

(deleted)

(deleted)

#### 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.

(deleted)

(deleted)

#### 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.

#### Mohamed Al-Fahim (Jan 10 2021 at 04:00):

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

#### 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