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.
33825 commits 1 branch 0 tags 5.3 GiB
Find a file
Kim Morrison a9e6c41b54
feat: allow simplifying dite_not/decide_not with only Decidable (¬p) (#5263) 
These lemmas are mostly useful for ensuring confluence of `simp`, but
rarely useful in proofs. However they don't seem to have any negative
impact.
2024-09-09 11:46:20 +00:00
.github
doc
images
nix feat: Lake shared library (#5143) 2024-09-09 09:05:54 +00:00
releases_drafts chore: release notes for 4.11.0 (#5221) 2024-09-02 00:19:41 +00:00
script feat: Lake shared library (#5143) 2024-09-09 09:05:54 +00:00
src feat: allow simplifying dite_not/decide_not with only Decidable (¬p) (#5263) 2024-09-09 11:46:20 +00:00
stage0
tests chore: remove @[simp] from List.head_mem and similar (#5271) 2024-09-09 06:05:06 +00:00
.gitattributes
.gitignore
.ignore
CMakeLists.txt
CMakePresets.json
CODEOWNERS
CONTRIBUTING.md
debug.log feat: lake: Reservoir-related configuration for packages (#4770) 2024-09-02 16:07:08 +00:00
flake.lock
flake.nix
lean-toolchain
lean.code-workspace
LICENSE
LICENSES
README.md
RELEASES.md chore: release notes for 4.11.0 (#5221) 2024-09-02 00:19:41 +00:00

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 (documentation source: doc/make/index.md).