Zulip Chat Archive

Stream: new members

Topic: Lean Manual


Andrey Cheremskoy (Jan 06 2022 at 02:58):

I've notice in the Lean Manual that Tactics appears twice in section 10 and then in section 15.
Also these two sections has the same content.
image.png
Also I see that the issue is in the SUMMARY.md file.
So I can fix this by creating a PR if required. Or someone else can do it.


Last updated: Dec 20 2023 at 11:08 UTC