Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
| examples | ||
| Lake | ||
| .gitignore | ||
| Lake.lean | ||
| leanpkg.toml | ||
| LICENSE | ||
| README.md | ||
Lake
An overhaul of Leanpkg for Lean 4 where the package configuration and build scripts are written in Lean. Currently just a prototype. A more detailed README will come when the project has matured.