Zulip Chat Archive

Stream: new members

Topic: Lean 4 docs typos

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.

Kevin Buzzard (Dec 19 2020 at 18:19):

(deleted)

Rob Lewis (Dec 19 2020 at 18:20):

@Sebastian Ullrich ?

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.

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.

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

Patrick Massot (Dec 19 2020 at 18:23):

TLDR: we should wait a bit.

Patrick Massot (Dec 19 2020 at 18:23):

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

Last updated: Dec 20 2023 at 11:08 UTC