leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: lean4

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.
I created a PR with the fix for this issue.
https://github.com/leanprover/lean4/pull/927


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll