mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00

Files

Marc Huisinga 168c125cf5 chore: relative lean-toolchains (#12652 )

This PR changes all `lean-toolchain` to use relative toolchain paths
instead of `lean4` and `lean4-stage0` identifiers, which removes the
need for manually linking toolchains via Elan.

After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code
extension will be needed to edit core.

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

2026-02-25 10:23:35 +00:00

grove

chore: relative lean-toolchains (#12652 )

2026-02-25 10:23:35 +00:00

naming-tree.svg

chore: revert mistaken deletion (#8404 )

2025-05-19 12:14:09 +00:00

naming.md

chore: revert mistaken deletion (#8404 )

2025-05-19 12:14:09 +00:00

README.md

chore: revert mistaken deletion (#8404 )

2025-05-19 12:14:09 +00:00

style.md

chore: revert mistaken deletion (#8404 )

2025-05-19 12:14:09 +00:00

vision.md

chore: revert mistaken deletion (#8404 )

2025-05-19 12:14:09 +00:00

README.md

The Lean standard library

This directory contains development information about the Lean standard library. The user-facing documentation of the standard library is part of the Lean Language Reference.

Here you will find

the standard library vision document, including the call for contributions,
the standard library style guide, and
the standard library naming conventions.