max/lean4-htt: Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4. - maxgit: wireguard access, git repository.

max/lean4-htt

Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.

Find a file

Leonardo de Moura 0795acaf6a refactor(library/init/algebra): new transport from multiplicative to additive The motivation is to avoid the problems produced by the "declare as structure and then tag as class idiom" described in the file ring.lean.		2017-01-18 19:39:53 -08:00
bin	refactor(gitignore): remove old ignore entries	2016-12-10 08:42:39 -08:00
doc	chore(doc/make/cygwin): we do not support cygwin anymore (only MSYS2)	2016-12-23 10:01:08 -08:00
extras	chore(extra/latex/*): update to changes in syntax	2017-01-03 11:22:04 -08:00
images	chore(CMakeLists.txt): move Lean logo to make sure we can test leanemacs without installing Lean	2015-01-31 17:38:49 -08:00
library	refactor(library/init/algebra): new transport from multiplicative to additive	2017-01-18 19:39:53 -08:00
old_library	refactor(gitignore): remove old ignore entries	2016-12-10 08:42:39 -08:00
script	refactor(emacs/load-lean): install emacs dependencies directly from (M)ELPA	2016-12-02 16:50:50 -08:00
src	feat(library/init/meta/environment): add is_projection	2017-01-18 18:12:08 -08:00
tests	fix(library/equations_compiler/elim_match): fix #1318	2017-01-18 08:21:53 -08:00
tmp	refactor(library/debugger): move debugger to tools	2016-12-17 10:50:13 -08:00
.appveyor.yml	chore(.appveyor.yml): missing DLLs	2017-01-14 07:47:38 -08:00
.codecov.yml	feat(.travis.yml): add codecov	2016-12-02 17:01:58 -08:00
.gitignore	chore(.gitignore): ignore VSCode config file	2016-12-18 12:35:25 -08:00
.travis.yml	chore(.travis.yml): fix STATIC config	2017-01-14 08:55:02 -08:00
LICENSE	Add LICENSE file	2013-07-15 18:55:48 -07:00
README.md	workaround instruction for gperftools on macOS Sierra	2017-01-17 16:37:06 -08:00

README.md

License	Windows	Linux / macOS	Test Coverage

About

Requirements

C++11 compatible compiler
CMake
GMP (GNU multiprecision library)
MPFR (GNU MPFR Library)
(optional) gperftools (There is currently an issue with gperftools on macOS Sierra. For now, either don't install it, or pass the flag -DTCMALLOC=OFF to CMake when building to not use it.)

Installing required packages at

Windows

MSys2

Linux

Ubuntu 16.04

OS X

OS X 10.9

Build Instructions

Miscellaneous

Building Doxygen Documentation: doxygen src/Doxyfile
Coding Style
Library Style Conventions
Git Commit Conventions
Automatic Builds
Syntax Highlight Lean Code in LaTeX