Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
b4660c96a9
This PR adds grind annotations for `List/Array/Vector.ofFn` theorems and additional `List.Impl` find operations. The annotations are added to theorems that correspond to those already annotated in the List implementation, ensuring consistency across all three container types (List, Array, Vector) for ofFn operations and related functionality. Key theorems annotated include: - Element access theorems (`getElem_ofFn`, `getElem?_ofFn`) - Construction and conversion theorems (`ofFn_zero`, `toList_ofFn`, `toArray_ofFn`) - Membership theorems (`mem_ofFn`) - Head/tail operations (`back_ofFn`) - Monadic operations (`ofFnM_zero`, `toList_ofFnM`, `toArray_ofFnM`, `idRun_ofFnM`) - List.Impl find operations (`find?_singleton`, `find?_append`, `findSome?_singleton`, `findSome?_append`) |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.