Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
a69052e7ee
We will use the thread safe version for implementing persistent hash maps. The hash maps will be used to implement decision procedures and refactor the congruence closure and ematching modules. The persistent hash maps based on thread safe parrays are performant when most of the time there is a single thread updating them. We use a small hack to make sure we don't have any overhead for parray<T, false> i.e., the thread unsafe version used in the VM. |
||
|---|---|---|
| bin | ||
| doc | ||
| extras | ||
| images | ||
| leanpkg | ||
| library | ||
| old_library | ||
| script | ||
| src | ||
| tests | ||
| tmp | ||
| .appveyor.yml | ||
| .appveyor.yml.in | ||
| .clang-format | ||
| .codecov.yml | ||
| .gitignore | ||
| .travis.yml | ||
| .travis.yml.in | ||
| LICENSE | ||
| README.md | ||
| License | Windows | Linux / macOS | Test Coverage | Chat |
|---|---|---|---|---|
 |
 |
 |
 |
About
- Homepage
- Theorem Proving in Lean
- Standard Library
- Emacs Mode
- For HoTT mode, please use Lean2.
Requirements
- C++11 compatible compiler
- CMake
- GMP (GNU multiprecision library)
Build Instructions
Miscellaneous
- Building Doxygen Documentation:
doxygen src/Doxyfile - Coding Style
- Library Style Conventions
- Git Commit Conventions
- Automatic Builds
- Syntax Highlight Lean Code in LaTeX