Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
Remark: the attribute actions used by the frontend are all in IO. These actions access attributes by name, and need access to the IO.ref that contains all registered attributes in the system. |
||
|---|---|---|
| .github | ||
| bin | ||
| doc | ||
| gen | ||
| images | ||
| lean4-mode | ||
| library | ||
| script | ||
| src | ||
| tests | ||
| .appveyor.yml | ||
| .clang-format | ||
| .codecov.yml | ||
| .gitattributes | ||
| .gitignore | ||
| .travis.yml | ||
| default.nix | ||
| LICENSE | ||
| README.md | ||
We are currently developing Lean 4. Lean 3 is still the latest official release. This repository contains work in progress.
Important. Unless you are one of our collaborators
- We strongly suggest you use Lean 3.
- Pull requests are not welcome.
- New issues are not welcome, and will be closed without any feedback.