mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

David Thrane Christiansen 2bb27af0d4 chore: automatically create reference manual PR branches (#9033 )

This PR adds a Mathlib-like testing and feedback system for the
reference manual. Lean PRs will receive comments that reflect the status
of the language reference with respect to the PR.

2025-06-27 13:23:41 +00:00

dev

chore: automatically create reference manual PR branches (#9033 )

2025-06-27 13:23:41 +00:00

examples

chore: remove old documentation site (#7974 )

2025-05-14 14:31:33 +00:00

images

doc: update quickstart guide for new display name (#5193 )

2024-08-28 13:29:16 +00:00

latex

doc: upstream the Lean4 pygments lexer (#3125 )

2024-05-20 11:40:24 +00:00

make

fix: indicate dependency on pkgconf in ubuntu docs (#6646 )

2025-01-15 05:30:20 +00:00

std

chore: Grove: high-level sections (#9011 )

2025-06-26 13:06:56 +00:00

.gitignore

doc: mdbook init

2020-10-30 14:23:47 +01:00

BoolExpr.lean

chore: Std -> Batteries renaming (#4108 )

2024-05-08 05:04:25 +00:00

metaprogramming-arith.lean

refactor: remove some unnecessary antiquotation kind annotations

2022-07-23 17:09:32 +02:00

perf.md

doc: add basic perf documentation

2021-09-06 07:12:36 -07:00

README.md

chore: remove old documentation site (#7974 )

2025-05-14 14:31:33 +00:00

style.md

doc: add documentation style guide (#8199 )

2025-05-02 13:05:18 +00:00

syntax_example.lean

doc: fix example style

2022-04-22 16:26:16 +02:00

README.md

Developer Documentation and Examples

This directory contains documentation that describes how to work on Lean itself, as well as examples that are included in documentation that's hosted on the Lean website. The make directory contains information on building Lean, and the dev directory describes how to work on Lean.

The documentation section has links to documentation that describes how to use Lean itself.