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.
24968 commits 1 branch 0 tags 5.3 GiB
Find a file
Daniel Fabian b7ecc1acc3 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-06-06 06:40:09 -07:00
.github chore: restore LEANC_EXTRA_FLAGS 2021-06-06 15:34:44 +02:00
doc doc: clarify RFC issues 2021-06-04 14:12:59 +02:00
images
lean4-mode fix: lean4-mode: show latest file progress data 2021-06-05 17:13:28 +02:00
nix chore: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
script chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
src test: Add a bunch of test for structural recursion on predicates. 2021-06-06 06:40:09 -07:00
stage0 chore: update stage0 2021-06-06 15:32:58 +02:00
tests refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 2021-06-06 06:40:09 -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 feat: Lean.js can compile itself 2021-06-06 15:34:44 +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: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
flake.nix chore: restore LEANC_EXTRA_FLAGS 2021-06-06 15:34:44 +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.