sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity
39,599 Commits 4,240 Branches 120 Tags
0520de73742c2033b4fb1eb288a1bf406baa1404
Go to file
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
Wojciech Różowski 0520de7374 fix: respect @[cbv_opaque] in reduceRecMatcher and reduceProj (#12621) 
This PR fixes a bug where `reduceRecMatcher?` and `reduceProj?` bypassed
the `@[cbv_opaque]` attribute. These kernel-level reduction functions
use `whnf` internally, which does not know about `@[cbv_opaque]`. This
meant `@[cbv_opaque]` values were unfolded when they appeared as match
discriminants, recursor major premises, or projection targets. The fix
introduces `withCbvOpaqueGuard`, which wraps these calls with
`withCanUnfoldPred` to prevent `whnf` from unfolding `@[cbv_opaque]`
definitions.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-20 16:13:26 +00:00
.claude
chore: enable leanprover/skills plugin for Claude Code (#12609)
2026-02-20 12:35:32 +00:00
.github
feat: lazy initialization of closed terms (#12044)
2026-02-20 08:45:15 +00:00
doc
chore: improve release command PR status checking (#12536)
2026-02-17 21:21:30 +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: remove stale release draft notes (#12518)
2026-02-17 19:56:23 +00:00
script
fix: update bump branch toolchain to nightly for all repos (#12586)
2026-02-19 13:04:26 +00:00
src
fix: respect @[cbv_opaque] in reduceRecMatcher and reduceProj (#12621)
2026-02-20 16:13:26 +00:00
stage0
chore: update stage0
2026-02-20 13:32:43 +00:00
tests
fix: respect @[cbv_opaque] in reduceRecMatcher and reduceProj (#12621)
2026-02-20 16:13:26 +00:00
.gitattributes
doc: grove: update and add String data (#11551)
2025-12-08 16:49:37 +00:00
.gitignore
chore: enable leanprover/skills plugin for Claude Code (#12609)
2026-02-20 12:35:32 +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
chore: fix repeated cmake calls breaking the build (#12598)
2026-02-19 16:23:47 +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: update to c++20 (#12117)
2026-02-11 01:17:40 +00:00
flake.nix
chore: update to c++20 (#12117)
2026-02-11 01:17:40 +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%