sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity
38,925 Commits 4,240 Branches 120 Tags
db93fe1608548721853390a10cd40580fe7d22ae
Go to file
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
Joachim Breitner db93fe1608 refactor: move String.ofList to the Prelude (#12029) 
This PR moves `String.ofList` to `Init.Prelude`. It is a function that
the Lean kernel expects to be present and has special support for (when
reducing string literals). By moving this to `Init.Prelude`, all
declarations that are special to the kernel are in that single module.

(cherry picked from commit 9167b13afa
and aac353c6b9)
2026-01-20 15:00:20 +01:00
.claude
chore: add guidance to not merge PRs autonomously in release command (#11661)
2025-12-14 05:17:42 +00:00
.github
chore: fix CMakeLists.txt CI check
2025-12-14 19:04:11 +11:00
doc
chore: update release docs/scripts for lean-fro.org (#11648)
2025-12-13 11:06:17 +00:00
images
chore(CMakeLists.txt): move Lean logo to make sure we can test leanemacs without installing Lean
2015-01-31 17:38:49 -08:00
releases_drafts
chore: add release draft for the module system (#11359)
2025-11-26 15:01:07 +00:00
script
chore: add missing repositories to release_repos.yml
2025-12-14 23:34:30 +11:00
src
refactor: move String.ofList to the Prelude (#12029)
2026-01-20 15:00:20 +01:00
stage0
chore: update stage0
2025-12-13 09:57:36 +00:00
tests
fix: realizeValue should default to the private scope (#11748)
2025-12-20 18:08:43 -08:00
.gitattributes
doc: grove: update and add String data (#11551)
2025-12-08 16:49:37 +00:00
.gitignore
chore: add .vscode/settings.json to .gitignore (#10795)
2025-10-16 07:08:41 +00:00
.gitpod.Dockerfile
chore: add gitpod configuration (#6382)
2024-12-15 21:38:13 +00:00
.gitpod.yml
chore: add gitpod configuration (#6382)
2024-12-15 21:38:13 +00:00
.ignore
chore: ignore stage0/ (for rg etc.)
2022-03-18 15:28:20 +01:00
CMakeLists.txt
fix: cadical dynamic dependencies (#11475)
2025-12-02 13:54:26 +00:00
CMakePresets.json
chore: CI: enable leak sanitizer again (#11339)
2025-11-27 18:32:35 +00:00
CODEOWNERS
chore: make @hargoniX code owner of the compiler (#10732)
2025-10-10 04:43:38 +00:00
CONTRIBUTING.md
doc: triage
2024-07-26 18:24:06 +02:00
flake.lock
chore: robustify Nix shell (#8141)
2025-04-28 15:08:32 +00:00
flake.nix
chore: use lld if available for building core (#10694)
2025-10-08 16:47:30 +00:00
lean-toolchain
doc: VS Code dev setup (#2961)
2023-11-30 08:35:03 +00:00
lean.code-workspace
chore: lean.code-workspace: fix terminal cwd (#10802)
2025-10-16 20:19:12 +00:00
LICENSE
chore: remove LICENSE header that confused GitHub
2021-11-18 09:42:35 +01:00
LICENSES
feat: ship cadical (#4325)
2024-08-23 09:13:27 +00:00
README.md
doc: update URLs that are currently pointing to redirects (#10397)
2025-09-17 15:50:07 +00:00
RELEASES.md
chore: updates to release_checklist.md (#7817)
2025-04-04 03:45:36 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.

Reference in New Issue View Git Blame Copy Permalink
Description
No description provided
leanlean4
Readme 5 GiB
Languages
Lean 94.3%
C++ 4.1%
Python 0.6%
Shell 0.4%
CMake 0.3%