Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
Find a file
Cameron Zwarich 3331ed9bb1
fix: add Float32 to LCNF.builtinRuntimeTypes list (#6837)
This PR adds Float32 to the LCNF builtinRuntimeTypes list. This was
missed during the initial Float32 implementation, but this omission has
the side effect of lowering Float32 to obj in the IR.
2025-01-31 04:53:49 +00:00
.github fix: Windows stage0 linking (#6622) 2025-01-14 09:09:50 +01:00
doc doc: clarify that lean_initialize_runtime_module is implied by lean_initialize (#6677) 2025-01-28 10:12:59 +00:00
images
nix fix: Windows stage0 linking (#6622) 2025-01-14 09:09:50 +01:00
releases_drafts chore: cherry-pick release notes from releases/v4.15.0 and releases/v4.16.0 (#6520) 2025-01-04 01:25:33 +00:00
script chore: update release checklist (#6637) 2025-01-14 10:18:46 +00:00
src fix: add Float32 to LCNF.builtinRuntimeTypes list (#6837) 2025-01-31 04:53:49 +00:00
stage0 chore: update stage0 2025-01-29 19:45:27 +00:00
tests feat: include Case analyses trace in the grind error message (#6881) 2025-01-31 04:22:50 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore feat: support Lake for building Lean core oleans (#3886) 2024-06-13 16:18:24 +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: Windows stage0 linking (#6622) 2025-01-14 09:09:50 +01:00
CMakePresets.json fix: prevent Task.get deadlocks from threadpool starvation (#6758) 2025-01-23 23:01:39 +00:00
CODEOWNERS chore: adjust CODEOWNERS (#6327) 2024-12-10 08:37:20 +00:00
CONTRIBUTING.md doc: triage 2024-07-26 18:24:06 +02:00
flake.lock feat: ship cadical (#4325) 2024-08-23 09:13:27 +00:00
flake.nix fix: Windows stage0 linking (#6622) 2025-01-14 09:09:50 +01:00
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00
lean.code-workspace chore: add the lean4 extension to the vscode workspace (#3059) 2023-12-14 08:58:21 +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 chore: update documentation title and link README to reference (#6409) 2024-12-17 22:18:56 +00:00
RELEASES.md doc: fix broken code blocks in RELEASES.md (#6527) 2025-01-04 08:08:12 +00:00

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).