Zulip Chat Archive
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*andSort*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):
Mohamed Al-Fahim (Jan 10 2021 at 03:43):
Threads that are short enough and almost entirely about style can be simply linked to
Mohamed Al-Fahim (Jan 10 2021 at 03:49):
(deleted)
Mohamed Al-Fahim (Jan 10 2021 at 03:50):
(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.
Mohamed Al-Fahim (Jan 10 2021 at 03:55):
(deleted)
Mohamed Al-Fahim (Jan 10 2021 at 03:56):
(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: Dec 20 2023 at 11:08 UTC