max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
36560 commits 1 branch 0 tags 5.3 GiB
Find a file
Kim Morrison 34e98c2efc
feat: add Decidable (∃ i, P i) (#8734) 
This PR adds the missing instance
```
instance decidableExistsFin (P : Fin n → Prop) [DecidablePred P] : Decidable (∃ i, P i)
```
2025-06-12 02:58:37 +00:00
.github fix: pin version of softprops/action-gh-release (#8710) 2025-06-11 00:08:18 +00:00
doc chore: improvements to release checklist and scripts (#8586) 2025-06-10 22:56:06 +00:00
images
nix
releases_drafts
script chore: move benchmarking script to this repo (#8718) 2025-06-11 12:27:06 +00:00
src feat: add Decidable (∃ i, P i) (#8734) 2025-06-12 02:58:37 +00:00
stage0 chore: update stage0 2025-06-11 16:51:07 +00:00
tests feat: diseq splitting and non-chronological backtracking for linarith (#8733) 2025-06-12 02:49:35 +00:00
.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 chore: remove old documentation site (#7974) 2025-05-14 14:31:33 +00:00
RELEASES.md

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.