Zulip Chat Archive

Stream: general

Topic: Get started with Lean 3


Martin Dvořák (Dec 19 2022 at 05:56):

Could this page indicate that it is written for Lean 3 please?
https://leanprover-community.github.io/get_started.html

Kevin Buzzard (Dec 19 2022 at 07:09):

You can probably make the PR yourself (but I'm not sure which repo it is)

Martin Dvořák (Dec 19 2022 at 07:11):

I already made a PR with the same suggestion to a different page in the same repository, but nobody merged it. I guess I must ask the right people?

Eric Wieser (Dec 20 2022 at 18:04):

You should ping those PRs on #PR reviews, very few people check the PRs on repos that aren't mathlib


Last updated: Dec 20 2023 at 11:08 UTC