Zulip Chat Archive

Stream: new members

Topic: Lean 4 docs typos


view this post on Zulip Tom Ellis (Dec 19 2020 at 18:19):

Hello everyone, I am Tom Ellis. I have just started looking into Lean. I work at Microsoft Research, Cambridge UK on compilers and machine learning.

I have spotted a number of minor typos in the Lean 4 documentation. Does anyone know if the Lean maintainers would welcome PRs to fix these? I wasn't sure how to interpret the guidance in the FAQ.

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 18:19):

(deleted)

view this post on Zulip Rob Lewis (Dec 19 2020 at 18:20):

@Sebastian Ullrich ?

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 18:21):

Thanks for asking, by the way. The Lean devs have been extremely clear about not wanting any PRs or issues for quite a long time now. At some point this will change I guess, but it's not clear when.

view this post on Zulip Tom Ellis (Dec 19 2020 at 18:23):

Thanks @Kevin Buzzard, and thanks for your interesting videos and writing about Lean, which got me interested in the first place.

view this post on Zulip Patrick Massot (Dec 19 2020 at 18:23):

See conversation at https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/217770643 for a partial answer

view this post on Zulip Patrick Massot (Dec 19 2020 at 18:23):

TLDR: we should wait a bit.

view this post on Zulip Patrick Massot (Dec 19 2020 at 18:23):

(of course Sebastian should feel free to update his answer if needed).


Last updated: May 07 2021 at 00:30 UTC