michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Mirror of https://github.com/leanprover/lean2 in case it ever disappears
8688 commits 3 branches 0 tags 28 MiB
C++ 47.8%
Lean 41.8%
JetBrains MPS 5.4%
Emacs Lisp 2.1%
C 1%
Other 1.7%
Find a file
Floris van Doorn 5333dcfa02 remove print command in hott/init
2018-01-25 17:33:42 -05:00
bin fix(bin/linja): fix some file name escaping 2016-12-10 22:34:32 +01:00
doc doc(README/make): correct some build instructions 2017-01-18 22:57:07 +01:00
extras feat(lstlean.tex): add Omega, and fix ` and * 2016-07-09 10:20:21 -07:00
hott remove print command in hott/init 2018-01-25 17:33:42 -05: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 feat(hott): make Type.{0} impredicative 2017-02-10 12:04:08 -05:00
script fix(script/check_md_links.py): author name 2016-02-23 20:17:03 -05:00
src feat(hott): make Type.{0} impredicative 2017-02-10 12:04:08 -05:00
tests/lean chore(tests/lean/run/num_norm1): remove test for broken tactic 2016-12-30 13:59:58 -08:00
.gitignore feat(util/file_lock): add support for Windows 2015-12-14 10:07:26 -08:00
.travis.osx.yml fix(.travis.osx.yml): explicitly turn on multi-thread support 2015-05-06 02:37:31 -04:00
.travis.windows.yml fix(.travis.windows.yml): use cmake-2.8.11.2 2015-05-05 17:17:37 -04:00
.travis.yml fix(.travis.yml): add missing ';'s 2015-05-13 17:52:39 -04:00
LICENSE Add LICENSE file 2013-07-15 18:55:48 -07:00
README.md doc(README/make): correct some build instructions 2017-01-18 22:57:07 +01:00

README.md

This is a snapshot of the Lean 0.2 theorem prover. We have this separate repository because this version has special support for Homotopy Type Theory.

About

Requirements

Installing required packages at

Windows

Linux

OS X

Build Instructions

Miscellaneous