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.
24881 commits 1 branch 0 tags 5.3 GiB
Find a file
Daniel Fabian c426a816a1 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
2021-05-22 18:09:32 -07:00
.github chore: Nix CI: fall back to building locally if remote cache doesn't work 2021-05-06 22:07:03 +02:00
doc chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
images
lean4-mode fix: lean4-mode: inaccessibles highlighting 2021-03-28 17:56:28 +02:00
nix chore: Nix: cleanup 2021-05-21 17:17:54 +02:00
script chore: link lean using leanc 2021-03-06 10:17:50 +01:00
src refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 2021-05-22 18:09:32 -07:00
stage0 chore: update stage0 2021-05-21 19:21:08 -07:00
tests refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 2021-05-22 18:09:32 -07:00
tmp chore: remove tactic framework dependency 2020-11-10 14:32:58 -08:00
.gitattributes chore: restore marking stage0/ as binary files, which we lost at some point 2020-08-14 11:12:13 +02:00
.gitignore chore: ignore result files from nix build 2020-11-24 19:16:27 +01:00
CMakeLists.txt chore: use standard release build for stage 0 2020-10-12 10:34:48 +02:00
CONTRIBUTING.md doc: more changes 2021-05-13 16:11:57 -07:00
default.nix doc: setup 2021-01-03 13:21:58 +01:00
flake.lock chore: Nix: update VS Code 2021-04-11 23:03:56 +02:00
flake.nix fix: Nix: VS Code override 2021-04-21 12:21:02 +02:00
LICENSE
README.md doc: contribution guidelines & README update 2021-01-12 14:38:36 -08:00
shell.nix doc: update dev setup editor instructions 2021-02-02 17:30:51 +01:00

README.md

This is the repository for Lean 4, which is currently being released as milestone releases towards a first stable release. Lean 3 is still the latest stable release.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.